From 31c5c27115c12fddfff3b5142ea6bb8cec4e529a Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 13:56:17 +0100
Subject: [PATCH 1/6] Artinian spaces + basic theorems

---
 properties/P000226.md | 21 +++++++++++++++++++++
 theorems/T000821.md   |  9 +++++++++
 theorems/T000822.md   |  9 +++++++++
 theorems/T000823.md   |  9 +++++++++
 theorems/T000824.md   | 11 +++++++++++
 5 files changed, 59 insertions(+)
 create mode 100644 properties/P000226.md
 create mode 100644 theorems/T000821.md
 create mode 100644 theorems/T000822.md
 create mode 100644 theorems/T000823.md
 create mode 100644 theorems/T000824.md

diff --git a/properties/P000226.md b/properties/P000226.md
new file mode 100644
index 000000000..2614d60a6
--- /dev/null
+++ b/properties/P000226.md
@@ -0,0 +1,21 @@
+---
+uid: P000226
+name: Artinian
+refs:
+  - zb: "0392.54005"
+    name: Finite $T_0$-spaces and universal mappings. (Holsztyński, Pedersen)
+---
+
+A space for which every collection of open sets has a minimal element.
+
+Equivalently:
+- Every collection of closed sets has a maximal element.
+- The open sets satisfy the *descending chain condition*: There is no infinite strictly increasing sequence $O_1 \supsetneq O_2 \supsetneq \cdots$ of open sets.
+- The closed sets satisfy the *ascending chain condition*: There is no infinite strictly decreasing sequence $Y_1 \subsetneq Y_2 \subsetneq \cdots$ of closed sets.
+
+See Section 1 of {{zb:0392.54005}}.
+
+----
+#### Meta-properties
+
+- This property is hereditary.
diff --git a/theorems/T000821.md b/theorems/T000821.md
new file mode 100644
index 000000000..6cdfc15f5
--- /dev/null
+++ b/theorems/T000821.md
@@ -0,0 +1,9 @@
+---
+uid: T000818
+if:
+  P000078: true
+then:
+  P000226: true
+---
+
+Immediate from the definitions.
diff --git a/theorems/T000822.md b/theorems/T000822.md
new file mode 100644
index 000000000..9b9a40abc
--- /dev/null
+++ b/theorems/T000822.md
@@ -0,0 +1,9 @@
+---
+uid: T000818
+if:
+  P000226: true
+then:
+  P00090: true
+---
+
+For any $x \in X$, the collection of open neighborhoods of $x$ must have a minimal element.
diff --git a/theorems/T000823.md b/theorems/T000823.md
new file mode 100644
index 000000000..e643d5de1
--- /dev/null
+++ b/theorems/T000823.md
@@ -0,0 +1,9 @@
+---
+uid: T000818
+if:
+  P000129: true
+then:
+  P000226: true
+---
+
+All collections of open sets are finite.
diff --git a/theorems/T000824.md b/theorems/T000824.md
new file mode 100644
index 000000000..76a526d2b
--- /dev/null
+++ b/theorems/T000824.md
@@ -0,0 +1,11 @@
+---
+uid: T000824
+if:
+  and:
+  - P000078: false
+  - P000002: true
+then:
+  P000226: false
+---
+
+Pick some $\{x_1,x_2,\dots\}\subseteq X$. Then $\{x_1\}\subsetneq \{x_1,x_2\}\subsetneq\{x_1,x_2,_x3\}, \dots$ is an infinite ascending chain of closed subsets.

From e4736125543bd8c57278ac3f21e4f04893bd3a0e Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 13:57:52 +0100
Subject: [PATCH 2/6] wrong iud's

---
 theorems/T000821.md | 2 +-
 theorems/T000822.md | 2 +-
 theorems/T000823.md | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theorems/T000821.md b/theorems/T000821.md
index 6cdfc15f5..e5da16c5b 100644
--- a/theorems/T000821.md
+++ b/theorems/T000821.md
@@ -1,5 +1,5 @@
 ---
-uid: T000818
+uid: T000821
 if:
   P000078: true
 then:
diff --git a/theorems/T000822.md b/theorems/T000822.md
index 9b9a40abc..0e4a3bc98 100644
--- a/theorems/T000822.md
+++ b/theorems/T000822.md
@@ -1,5 +1,5 @@
 ---
-uid: T000818
+uid: T000822
 if:
   P000226: true
 then:
diff --git a/theorems/T000823.md b/theorems/T000823.md
index e643d5de1..3c6885b16 100644
--- a/theorems/T000823.md
+++ b/theorems/T000823.md
@@ -1,5 +1,5 @@
 ---
-uid: T000818
+uid: T000823
 if:
   P000129: true
 then:

From f875009cf9528656baac24a2ba1405c9dcf0f88f Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 13:59:09 +0100
Subject: [PATCH 3/6] missing 0

---
 theorems/T000822.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000822.md b/theorems/T000822.md
index 0e4a3bc98..747a5c7ee 100644
--- a/theorems/T000822.md
+++ b/theorems/T000822.md
@@ -3,7 +3,7 @@ uid: T000822
 if:
   P000226: true
 then:
-  P00090: true
+  P000090: true
 ---
 
 For any $x \in X$, the collection of open neighborhoods of $x$ must have a minimal element.

From ff0847c19eacd60570b8f5d707c5f42bf79c8bb2 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Fri, 2 Jan 2026 14:26:28 +0100
Subject: [PATCH 4/6] changed id of theorems

---
 theorems/{T000821.md => T000825.md} | 2 +-
 theorems/{T000822.md => T000826.md} | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename theorems/{T000821.md => T000825.md} (86%)
 rename theorems/{T000822.md => T000826.md} (91%)

diff --git a/theorems/T000821.md b/theorems/T000825.md
similarity index 86%
rename from theorems/T000821.md
rename to theorems/T000825.md
index e5da16c5b..ae671e426 100644
--- a/theorems/T000821.md
+++ b/theorems/T000825.md
@@ -1,5 +1,5 @@
 ---
-uid: T000821
+uid: T000825
 if:
   P000078: true
 then:
diff --git a/theorems/T000822.md b/theorems/T000826.md
similarity index 91%
rename from theorems/T000822.md
rename to theorems/T000826.md
index 747a5c7ee..72963bddf 100644
--- a/theorems/T000822.md
+++ b/theorems/T000826.md
@@ -1,5 +1,5 @@
 ---
-uid: T000822
+uid: T000826
 if:
   P000226: true
 then:

From e113028f18e30ac3199cf12881dea336b6653788 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Fri, 2 Jan 2026 16:16:06 +0100
Subject: [PATCH 5/6] Update P000226.md

---
 properties/P000226.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/properties/P000226.md b/properties/P000226.md
index 2614d60a6..b15ceccc3 100644
--- a/properties/P000226.md
+++ b/properties/P000226.md
@@ -10,8 +10,8 @@ A space for which every collection of open sets has a minimal element.
 
 Equivalently:
 - Every collection of closed sets has a maximal element.
-- The open sets satisfy the *descending chain condition*: There is no infinite strictly increasing sequence $O_1 \supsetneq O_2 \supsetneq \cdots$ of open sets.
-- The closed sets satisfy the *ascending chain condition*: There is no infinite strictly decreasing sequence $Y_1 \subsetneq Y_2 \subsetneq \cdots$ of closed sets.
+- The open sets satisfy the *descending chain condition*: There is no infinite strictly decreasing sequence $O_1 \supsetneq O_2 \supsetneq \cdots$ of open sets.
+- The closed sets satisfy the *ascending chain condition*: There is no infinite strictly increasing sequence $Y_1 \subsetneq Y_2 \subsetneq \cdots$ of closed sets.
 
 See Section 1 of {{zb:0392.54005}}.
 

From 111225139889302e0896611c500c0012b1b28aec Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 16:58:40 +0100
Subject: [PATCH 6/6] apply suggestion

---
 theorems/T000824.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000824.md b/theorems/T000824.md
index 76a526d2b..685690fcd 100644
--- a/theorems/T000824.md
+++ b/theorems/T000824.md
@@ -8,4 +8,4 @@ then:
   P000226: false
 ---
 
-Pick some $\{x_1,x_2,\dots\}\subseteq X$. Then $\{x_1\}\subsetneq \{x_1,x_2\}\subsetneq\{x_1,x_2,_x3\}, \dots$ is an infinite ascending chain of closed subsets.
+Pick distinct $x_1,x_2,\dots\in X$. Then $\{x_1\}\subsetneq \{x_1,x_2\}\subsetneq\{x_1, x_2, x_3\} \subsetneq \dots$ is an infinite ascending chain of closed subsets.