From 6bcd3927bed1edb83a4bc85802e37bd941fce45d Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 22:46:07 +0100
Subject: [PATCH 01/34] A few theorems for artinian

---
 theorems/T000827.md | 11 +++++++++++
 theorems/T000828.md | 11 +++++++++++
 theorems/T000829.md | 11 +++++++++++
 theorems/T000830.md | 11 +++++++++++
 4 files changed, 44 insertions(+)
 create mode 100644 theorems/T000827.md
 create mode 100644 theorems/T000828.md
 create mode 100644 theorems/T000829.md
 create mode 100644 theorems/T000830.md

diff --git a/theorems/T000827.md b/theorems/T000827.md
new file mode 100644
index 000000000..2aff2c296
--- /dev/null
+++ b/theorems/T000827.md
@@ -0,0 +1,11 @@
+---
+uid: T000827
+if:
+  and:
+  - P000078: false
+  - P000203: true
+then:
+  P000226: false
+---
+
+Note that if $p\in X$ is the isolated point and $x \in X$, we must have $\operatorname{cl}(x)\subseteq \{x,p\}$. A similar argument as in {T824} thus proves the assertion.
diff --git a/theorems/T000828.md b/theorems/T000828.md
new file mode 100644
index 000000000..300b98710
--- /dev/null
+++ b/theorems/T000828.md
@@ -0,0 +1,11 @@
+---
+uid: T000828
+if:
+  and:
+  - P000047: true
+  - P000226: true
+then:
+  P000078: true
+---
+
+Immediate consequence of Proposition 2.6 from [this](https://pjm.ppu.edu/sites/default/files/papers/PJM_12%282%29_2023_201_to_207.pdf) paper.
diff --git a/theorems/T000829.md b/theorems/T000829.md
new file mode 100644
index 000000000..70ba835b1
--- /dev/null
+++ b/theorems/T000829.md
@@ -0,0 +1,11 @@
+---
+uid: T000829
+if:
+  and:
+  - P000045: true
+  - P000226: true
+then:
+  P000078: true
+---
+
+Since {P226} is hereditary, this follows from {T828}.
diff --git a/theorems/T000830.md b/theorems/T000830.md
new file mode 100644
index 000000000..9db226459
--- /dev/null
+++ b/theorems/T000830.md
@@ -0,0 +1,11 @@
+---
+uid: T000830
+if:
+  and:
+  - P000185: true
+  - P000226: true
+then:
+  P000016: true
+---
+
+Clearly a {P185} is {P16} iff it has finitely many open sets. Since {P226} extends to the Kolmogorov quotient, the assertion follow from {T824}.

From e14807cbf2e893571513f451fd665e062f36bfcb Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 22:48:13 +0100
Subject: [PATCH 02/34] add metaproperty

---
 properties/P000226.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/properties/P000226.md b/properties/P000226.md
index b15ceccc3..dde4ca7fa 100644
--- a/properties/P000226.md
+++ b/properties/P000226.md
@@ -15,7 +15,10 @@ Equivalently:
 
 See Section 1 of {{zb:0392.54005}}.
 
+Compare this property with {P208}.
+
 ----
 #### Meta-properties
 
 - This property is hereditary.
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.

From 460acfdadec93fb6a13e93d60b6cd76fff4ff182 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 2 Jan 2026 22:51:58 +0100
Subject: [PATCH 03/34] typo

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

diff --git a/theorems/T000827.md b/theorems/T000827.md
index 2aff2c296..29d156445 100644
--- a/theorems/T000827.md
+++ b/theorems/T000827.md
@@ -8,4 +8,4 @@ then:
   P000226: false
 ---
 
-Note that if $p\in X$ is the isolated point and $x \in X$, we must have $\operatorname{cl}(x)\subseteq \{x,p\}$. A similar argument as in {T824} thus proves the assertion.
+Note that if $p\in X$ is the non-isolated point and $x \in X$, we must have $\operatorname{cl}(x)\subseteq \{x,p\}$. A similar argument as in {T824} thus proves the assertion.

From 88050f8fa9fe94d074377f9f91c9f0d50febfad7 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Fri, 2 Jan 2026 18:16:30 -0500
Subject: [PATCH 04/34] P226 minor tweaks

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

diff --git a/properties/P000226.md b/properties/P000226.md
index dde4ca7fa..4147b7bb6 100644
--- a/properties/P000226.md
+++ b/properties/P000226.md
@@ -6,16 +6,16 @@ refs:
     name: Finite $T_0$-spaces and universal mappings. (Holsztyński, Pedersen)
 ---
 
-A space for which every collection of open sets has a minimal element.
+Every nonempty collection of open sets has a minimal element.
 
 Equivalently:
-- Every collection of closed sets has a maximal element.
+- Every nonempty collection of closed sets has a maximal element.
 - 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}}.
 
-Compare this property with {P208}.
+Compare with {P208}.
 
 ----
 #### Meta-properties

From 14b10efb672510b43c531273c4c5d2bddfaab884 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 00:42:38 +0100
Subject: [PATCH 05/34] contrapose

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

diff --git a/theorems/T000830.md b/theorems/T000830.md
index 9db226459..4cdf0ace8 100644
--- a/theorems/T000830.md
+++ b/theorems/T000830.md
@@ -3,9 +3,9 @@ uid: T000830
 if:
   and:
   - P000185: true
-  - P000226: true
+  - P000016: false
 then:
-  P000016: true
+  P000226: false
 ---
 
 Clearly a {P185} is {P16} iff it has finitely many open sets. Since {P226} extends to the Kolmogorov quotient, the assertion follow from {T824}.

From edc544d7c635e38d40e0ba94e4c937e637f58877 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 00:44:59 +0100
Subject: [PATCH 06/34] rephrase 226

---
 theorems/T000824.md | 6 +++---
 theorems/T000830.md | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theorems/T000824.md b/theorems/T000824.md
index 685690fcd..848cdbdd6 100644
--- a/theorems/T000824.md
+++ b/theorems/T000824.md
@@ -2,10 +2,10 @@
 uid: T000824
 if:
   and:
-  - P000078: false
+  - P000226: true
   - P000002: true
 then:
-  P000226: false
+  P000078: true
 ---
 
-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.
+Assume $X$ were infinite. 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, contradiction to {P226}.
diff --git a/theorems/T000830.md b/theorems/T000830.md
index 4cdf0ace8..89abfcfce 100644
--- a/theorems/T000830.md
+++ b/theorems/T000830.md
@@ -3,9 +3,9 @@ uid: T000830
 if:
   and:
   - P000185: true
-  - P000016: false
+  - P000226: false
 then:
-  P000226: false
+  P000016: true
 ---
 
 Clearly a {P185} is {P16} iff it has finitely many open sets. Since {P226} extends to the Kolmogorov quotient, the assertion follow from {T824}.

From a1123d009167592ef350658a4e216570cbe10ad4 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 01:07:41 +0100
Subject: [PATCH 07/34] Apply suggestion from @yhx-12243

Co-authored-by: yhx-12243 <yhx12243@gmail.com>
---
 theorems/T000830.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000830.md b/theorems/T000830.md
index 89abfcfce..9db226459 100644
--- a/theorems/T000830.md
+++ b/theorems/T000830.md
@@ -3,7 +3,7 @@ uid: T000830
 if:
   and:
   - P000185: true
-  - P000226: false
+  - P000226: true
 then:
   P000016: true
 ---

From b77a680c472107911215be8ea79af881e88ef566 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 01:12:11 +0100
Subject: [PATCH 08/34] Update theorems/T000827.md

Co-authored-by: yhx-12243 <yhx12243@gmail.com>
---
 theorems/T000827.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theorems/T000827.md b/theorems/T000827.md
index 29d156445..8393daf8a 100644
--- a/theorems/T000827.md
+++ b/theorems/T000827.md
@@ -2,10 +2,10 @@
 uid: T000827
 if:
   and:
-  - P000078: false
   - P000203: true
+  - P000226: true
 then:
-  P000226: false
+  P000078: true
 ---
 
 Note that if $p\in X$ is the non-isolated point and $x \in X$, we must have $\operatorname{cl}(x)\subseteq \{x,p\}$. A similar argument as in {T824} thus proves the assertion.

From e6b223f964d8a8e2b2e9c0609f0e59e1a6582cc5 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 03:11:24 +0100
Subject: [PATCH 09/34] scattered + separable

---
 theorems/T000829.md |  8 +++-----
 theorems/T000831.md | 16 ++++++++++++++++
 theorems/T000832.md |  0
 3 files changed, 19 insertions(+), 5 deletions(-)
 create mode 100644 theorems/T000831.md
 create mode 100644 theorems/T000832.md

diff --git a/theorems/T000829.md b/theorems/T000829.md
index 70ba835b1..94db4af62 100644
--- a/theorems/T000829.md
+++ b/theorems/T000829.md
@@ -1,11 +1,9 @@
 ---
 uid: T000829
 if:
-  and:
-  - P000045: true
-  - P000226: true
+  P000226: true
 then:
-  P000078: true
+  P000026: true
 ---
 
-Since {P226} is hereditary, this follows from {T828}.
+Consider the collection of closed set $\mathcal{C}:=\{\operatorname{cl}(C)\mid \text{$C\subseteq X$ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\}) \in \mathcal{C}$, contradiction.
diff --git a/theorems/T000831.md b/theorems/T000831.md
new file mode 100644
index 000000000..56631a08a
--- /dev/null
+++ b/theorems/T000831.md
@@ -0,0 +1,16 @@
+---
+uid: T000831
+if:
+  and:
+  - P000001: true
+  - P000226: true
+then:
+  P000051: true
+---
+
+For $x \in X$, let $U_x\subseteq X$ be its minimal open neighborhood, this is well-defined by {T824}.
+Let $U_z$ be a minimal member of the collection \{U_x\mid x \in X\}.
+
+Suppose $U_z$ contains $y \neq z$. Then by {P1} it follows $U_y \subsetneq U_z$, contradiction.
+
+Therefore $X$ has an isolated point. Since both {P1} and {P226} are hereditary, the assertion follows.
diff --git a/theorems/T000832.md b/theorems/T000832.md
new file mode 100644
index 000000000..e69de29bb

From 5943b735bdc1382346cb1a26e08544af4288e3d4 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 03:14:38 +0100
Subject: [PATCH 10/34] wrong file

---
 theorems/T000829.md | 8 +++++---
 theorems/T000832.md | 9 +++++++++
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/theorems/T000829.md b/theorems/T000829.md
index 94db4af62..70ba835b1 100644
--- a/theorems/T000829.md
+++ b/theorems/T000829.md
@@ -1,9 +1,11 @@
 ---
 uid: T000829
 if:
-  P000226: true
+  and:
+  - P000045: true
+  - P000226: true
 then:
-  P000026: true
+  P000078: true
 ---
 
-Consider the collection of closed set $\mathcal{C}:=\{\operatorname{cl}(C)\mid \text{$C\subseteq X$ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\}) \in \mathcal{C}$, contradiction.
+Since {P226} is hereditary, this follows from {T828}.
diff --git a/theorems/T000832.md b/theorems/T000832.md
index e69de29bb..52bf44027 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -0,0 +1,9 @@
+---
+uid: T000832
+if:
+  P000226: true
+then:
+  P000026: true
+---
+
+Consider the collection of closed set $\mathcal{C}:=\{\operatorname{cl}(C)\mid \text{$C\subseteq X$ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\}) \in \mathcal{C}$, contradiction.

From 09b2b0c3b4fce9e8ffb8229519ca375258b21978 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 03:17:57 +0100
Subject: [PATCH 11/34] hopefully fix latex error

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

diff --git a/theorems/T000832.md b/theorems/T000832.md
index 52bf44027..5313ce9cd 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -6,4 +6,4 @@ then:
   P000026: true
 ---
 
-Consider the collection of closed set $\mathcal{C}:=\{\operatorname{cl}(C)\mid \text{$C\subseteq X$ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\}) \in \mathcal{C}$, contradiction.
+Consider the collection of closed sets $\{\operatorname{cl}(C)\mid \text{$C\subseteq X$ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\})$, contradiction.

From f7acbcf8d66305448d955b7c48521bf30dac8751 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Sat, 3 Jan 2026 07:07:41 +0100
Subject: [PATCH 12/34] Update theorems/T000831.md

Co-authored-by: yhx-12243 <yhx12243@gmail.com>
---
 theorems/T000831.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000831.md b/theorems/T000831.md
index 56631a08a..2d1b682d8 100644
--- a/theorems/T000831.md
+++ b/theorems/T000831.md
@@ -9,7 +9,7 @@ then:
 ---
 
 For $x \in X$, let $U_x\subseteq X$ be its minimal open neighborhood, this is well-defined by {T824}.
-Let $U_z$ be a minimal member of the collection \{U_x\mid x \in X\}.
+Let $U_z$ be a minimal member of the collection $\{U_x\mid x \in X\}$.
 
 Suppose $U_z$ contains $y \neq z$. Then by {P1} it follows $U_y \subsetneq U_z$, contradiction.
 

From ad8ce2d7b89f91e98d9a69ee7d42765d2979c385 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Sat, 3 Jan 2026 07:08:17 +0100
Subject: [PATCH 13/34] Update theorems/T000832.md

Co-authored-by: yhx-12243 <yhx12243@gmail.com>
---
 theorems/T000832.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000832.md b/theorems/T000832.md
index 5313ce9cd..c02ea002c 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -6,4 +6,4 @@ then:
   P000026: true
 ---
 
-Consider the collection of closed sets $\{\operatorname{cl}(C)\mid \text{$C\subseteq X$ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\})$, contradiction.
+Consider the collection of closed sets $\{\operatorname{cl}(C)\mid C\subseteq X\text{ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\})$, contradiction.

From d70482bbda393b65894993330e8a39c75646590d Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 16:47:15 +0100
Subject: [PATCH 14/34] updates

---
 properties/P000226.md |  4 +++-
 theorems/T000828.md   | 11 -----------
 theorems/T000829.md   |  2 +-
 theorems/T000831.md   | 14 +++++++-------
 4 files changed, 11 insertions(+), 20 deletions(-)
 delete mode 100644 theorems/T000828.md

diff --git a/properties/P000226.md b/properties/P000226.md
index 4147b7bb6..3dbb270f8 100644
--- a/properties/P000226.md
+++ b/properties/P000226.md
@@ -4,6 +4,7 @@ name: Artinian
 refs:
   - zb: "0392.54005"
     name: Finite $T_0$-spaces and universal mappings. (Holsztyński, Pedersen)
+  - mathse: 5117935
 ---
 
 Every nonempty collection of open sets has a minimal element.
@@ -12,8 +13,9 @@ Equivalently:
 - Every nonempty collection of closed sets has a maximal element.
 - 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.
+- Every subset has a finite dense subset.
 
-See Section 1 of {{zb:0392.54005}}.
+See {{mathse:5117935}} for a proof of the equivalences.
 
 Compare with {P208}.
 
diff --git a/theorems/T000828.md b/theorems/T000828.md
deleted file mode 100644
index 300b98710..000000000
--- a/theorems/T000828.md
+++ /dev/null
@@ -1,11 +0,0 @@
----
-uid: T000828
-if:
-  and:
-  - P000047: true
-  - P000226: true
-then:
-  P000078: true
----
-
-Immediate consequence of Proposition 2.6 from [this](https://pjm.ppu.edu/sites/default/files/papers/PJM_12%282%29_2023_201_to_207.pdf) paper.
diff --git a/theorems/T000829.md b/theorems/T000829.md
index 70ba835b1..098e36f02 100644
--- a/theorems/T000829.md
+++ b/theorems/T000829.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Since {P226} is hereditary, this follows from {T828}.
+Since {P226} is hereditary and {P47} implies {P2}, this follows from {T824}.
diff --git a/theorems/T000831.md b/theorems/T000831.md
index 2d1b682d8..0b32d91ab 100644
--- a/theorems/T000831.md
+++ b/theorems/T000831.md
@@ -2,15 +2,15 @@
 uid: T000831
 if:
   and:
-  - P000001: true
   - P000226: true
+  - P000001: true
 then:
   P000051: true
 ---
 
-For $x \in X$, let $U_x\subseteq X$ be its minimal open neighborhood, this is well-defined by {T824}.
-Let $U_z$ be a minimal member of the collection $\{U_x\mid x \in X\}$.
-
-Suppose $U_z$ contains $y \neq z$. Then by {P1} it follows $U_y \subsetneq U_z$, contradiction.
-
-Therefore $X$ has an isolated point. Since both {P1} and {P226} are hereditary, the assertion follows.
+Let $A$ be a nonempty subset of $X$.  
+Let $U$ be a minimal open set in $X$ with $U\cap A\ne\emptyset$.  
+The set $U\cap A$ cannot contain two distinct points;  
+otherwise, by the {P1} property there would be an open set $V$ in $X$ containing one point and not the other.  
+Then $U\cap V$ would be a strictly smaller open set that meets $A$, which is not possible.  
+Thus, the element of $U\cap A$ is isolated in $A$.

From 161cf849fc95f5d06a1deeb8cd6b997e4526bd83 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 16:47:57 +0100
Subject: [PATCH 15/34] replace subset with subspace

---
 properties/P000226.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/properties/P000226.md b/properties/P000226.md
index 3dbb270f8..a10e5c492 100644
--- a/properties/P000226.md
+++ b/properties/P000226.md
@@ -13,7 +13,7 @@ Equivalently:
 - Every nonempty collection of closed sets has a maximal element.
 - 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.
-- Every subset has a finite dense subset.
+- Every subspace has a finite dense subset.
 
 See {{mathse:5117935}} for a proof of the equivalences.
 

From 5e0a35a8f41c2da2d0b9a85c62897838a7265918 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 16:52:46 +0100
Subject: [PATCH 16/34] add name

---
 properties/P000226.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/properties/P000226.md b/properties/P000226.md
index a10e5c492..20e8bd8a4 100644
--- a/properties/P000226.md
+++ b/properties/P000226.md
@@ -5,6 +5,7 @@ refs:
   - zb: "0392.54005"
     name: Finite $T_0$-spaces and universal mappings. (Holsztyński, Pedersen)
   - mathse: 5117935
+    name: Equivalent definitions of an Artinian space
 ---
 
 Every nonempty collection of open sets has a minimal element.

From eed0246ba5791695f4aab01d930406cf1a1e7156 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 16:58:34 +0100
Subject: [PATCH 17/34] update separable

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

diff --git a/theorems/T000832.md b/theorems/T000832.md
index c02ea002c..e2f11c794 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -6,4 +6,4 @@ then:
   P000026: true
 ---
 
-Consider the collection of closed sets $\{\operatorname{cl}(C)\mid C\subseteq X\text{ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\})$, contradiction.
+Immediate from (one of the equivalent) the definitions.

From 1875c5b979eb9808b290321cd405de3d2d104401 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 17:32:01 +0100
Subject: [PATCH 18/34] Update theorems/T000832.md

Co-authored-by: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
---
 theorems/T000832.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000832.md b/theorems/T000832.md
index e2f11c794..82f5431fd 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -6,4 +6,4 @@ then:
   P000026: true
 ---
 
-Immediate from (one of the equivalent) the definitions.
+From definitions.

From 66d6b441e4376a9dcd750e4714c59b83ce8fbf42 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 17:32:49 +0100
Subject: [PATCH 19/34] Update theorems/T000830.md

Co-authored-by: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
---
 theorems/T000830.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000830.md b/theorems/T000830.md
index 9db226459..b0ab1afdc 100644
--- a/theorems/T000830.md
+++ b/theorems/T000830.md
@@ -8,4 +8,4 @@ then:
   P000016: true
 ---
 
-Clearly a {P185} is {P16} iff it has finitely many open sets. Since {P226} extends to the Kolmogorov quotient, the assertion follow from {T824}.
+If $X$ is a {P185}, then $X$ is {P16} iff the Kolmogorov quotient $\text{Kol}(X)$ is finite. The assertion then follows from {T824}.

From 30179d8aec9873a261dd5a63e5617a8aabcc5588 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 17:38:34 +0100
Subject: [PATCH 20/34] Update theorems/T000829.md

Co-authored-by: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
---
 theorems/T000829.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000829.md b/theorems/T000829.md
index 098e36f02..76bf75c47 100644
--- a/theorems/T000829.md
+++ b/theorems/T000829.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Since {P226} is hereditary and {P47} implies {P2}, this follows from {T824}.
+Since {P226} is hereditary and {P47} implies {P2} ([explore](https://topology.pi-base.org/spaces?q=47+%2B+not+2)), this follows from {T824}.

From 558a8609cf79a3497bdaa712606606d37dd66219 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 17:39:05 +0100
Subject: [PATCH 21/34] Update theorems/T000832.md

Co-authored-by: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
---
 theorems/T000832.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000832.md b/theorems/T000832.md
index 82f5431fd..9aee572f5 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -3,7 +3,7 @@ uid: T000832
 if:
   P000226: true
 then:
-  P000026: true
+  P000180: true
 ---
 
 From definitions.

From 22180aa7daf900af7819e9de01ca9c78f3cb574a Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 18:38:51 +0100
Subject: [PATCH 22/34] Update theorems/T000824.md

Co-authored-by: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
---
 theorems/T000824.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000824.md b/theorems/T000824.md
index 848cdbdd6..abacf3e13 100644
--- a/theorems/T000824.md
+++ b/theorems/T000824.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Assume $X$ were infinite. 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, contradiction to {P226}.
+Since $X$ is {P226} we can find finite dense set $F\subseteq X$. Since $X$ is {P2}, $F$ is closed, so $F = X$.

From eef47b6a7b362e50e082fe79dbb017cbed1f45b5 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 19:22:57 +0100
Subject: [PATCH 23/34] rewrite 827

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

diff --git a/theorems/T000827.md b/theorems/T000827.md
index 8393daf8a..fda2b7f17 100644
--- a/theorems/T000827.md
+++ b/theorems/T000827.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Note that if $p\in X$ is the non-isolated point and $x \in X$, we must have $\operatorname{cl}(x)\subseteq \{x,p\}$. A similar argument as in {T824} thus proves the assertion.
+Let $p \in X$ be the non-isolated point. Since {P226} is hereditary, the discrete space $X \setminus \{p\}$ (and by extension $X$) must be finite by {T824}.

From 9e2af5c585ba2d2799260067923ff2c16140b9dd Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 19:57:35 +0100
Subject: [PATCH 24/34] two more theorems

---
 theorems/T000828.md | 9 +++++++++
 theorems/T000833.md | 9 +++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 theorems/T000828.md
 create mode 100644 theorems/T000833.md

diff --git a/theorems/T000828.md b/theorems/T000828.md
new file mode 100644
index 000000000..f9aadc7f8
--- /dev/null
+++ b/theorems/T000828.md
@@ -0,0 +1,9 @@
+---
+uid: T000828
+if:
+  P000226: true
+then:
+  P000021: true
+---
+
+Since {P226} is hereditary, this follows from {T42} and {T824}.
diff --git a/theorems/T000833.md b/theorems/T000833.md
new file mode 100644
index 000000000..093b02ba8
--- /dev/null
+++ b/theorems/T000833.md
@@ -0,0 +1,9 @@
+---
+uid: T000833
+if:
+  P000226: true
+then:
+  P000197: true
+---
+
+Since {P226} is hereditary, this follows from {T42} and {T824}.

From 8405576e7527c5c13c213fb2de70973baffa2017 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 3 Jan 2026 20:19:36 +0100
Subject: [PATCH 25/34] remove redundant

---
 theorems/T000833.md | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 theorems/T000833.md

diff --git a/theorems/T000833.md b/theorems/T000833.md
deleted file mode 100644
index 093b02ba8..000000000
--- a/theorems/T000833.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-uid: T000833
-if:
-  P000226: true
-then:
-  P000197: true
----
-
-Since {P226} is hereditary, this follows from {T42} and {T824}.

From 9ff040a807a4dd323e18b997ec6bd36c7bbc87ff Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Sat, 3 Jan 2026 14:19:50 -0500
Subject: [PATCH 26/34] flip order of hypotheses

---
 theorems/T000827.md | 2 +-
 theorems/T000829.md | 2 +-
 theorems/T000830.md | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theorems/T000827.md b/theorems/T000827.md
index fda2b7f17..4f331a9cc 100644
--- a/theorems/T000827.md
+++ b/theorems/T000827.md
@@ -2,8 +2,8 @@
 uid: T000827
 if:
   and:
-  - P000203: true
   - P000226: true
+  - P000203: true
 then:
   P000078: true
 ---
diff --git a/theorems/T000829.md b/theorems/T000829.md
index 76bf75c47..743d81a66 100644
--- a/theorems/T000829.md
+++ b/theorems/T000829.md
@@ -2,8 +2,8 @@
 uid: T000829
 if:
   and:
-  - P000045: true
   - P000226: true
+  - P000045: true
 then:
   P000078: true
 ---
diff --git a/theorems/T000830.md b/theorems/T000830.md
index b0ab1afdc..af0d7442a 100644
--- a/theorems/T000830.md
+++ b/theorems/T000830.md
@@ -2,8 +2,8 @@
 uid: T000830
 if:
   and:
-  - P000185: true
   - P000226: true
+  - P000185: true
 then:
   P000016: true
 ---

From 3a4d32c7645a0c24f8ffaa7a579e10fb87d1b0c0 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Sat, 3 Jan 2026 17:55:04 -0500
Subject: [PATCH 27/34] T831 fix whitespace problem

---
 theorems/T000831.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theorems/T000831.md b/theorems/T000831.md
index 0b32d91ab..11e148af7 100644
--- a/theorems/T000831.md
+++ b/theorems/T000831.md
@@ -8,9 +8,9 @@ then:
   P000051: true
 ---
 
-Let $A$ be a nonempty subset of $X$.  
-Let $U$ be a minimal open set in $X$ with $U\cap A\ne\emptyset$.  
-The set $U\cap A$ cannot contain two distinct points;  
-otherwise, by the {P1} property there would be an open set $V$ in $X$ containing one point and not the other.  
-Then $U\cap V$ would be a strictly smaller open set that meets $A$, which is not possible.  
+Let $A$ be a nonempty subset of $X$.
+Let $U$ be a minimal open set in $X$ with $U\cap A\ne\emptyset$.
+The set $U\cap A$ cannot contain two distinct points;
+otherwise, by the {P1} property there would be an open set $V$ in $X$ containing one point and not the other.
+Then $U\cap V$ would be a strictly smaller open set that meets $A$, which is not possible.
 Thus, the element of $U\cap A$ is isolated in $A$.

From 63d4951dc1fee9f3b623d14ffcead467ed4ebe72 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sun, 4 Jan 2026 00:29:55 +0100
Subject: [PATCH 28/34] Update theorems/T000832.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000832.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000832.md b/theorems/T000832.md
index 9aee572f5..355b16d5b 100644
--- a/theorems/T000832.md
+++ b/theorems/T000832.md
@@ -6,4 +6,4 @@ then:
   P000180: true
 ---
 
-From definitions.
+Immediate from the definitions.

From aa12fa4545a0cd86ba1465e53a7072d27b013ab7 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sun, 4 Jan 2026 00:30:04 +0100
Subject: [PATCH 29/34] Update theorems/T000824.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000824.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000824.md b/theorems/T000824.md
index abacf3e13..dc1c989fa 100644
--- a/theorems/T000824.md
+++ b/theorems/T000824.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Since $X$ is {P226} we can find finite dense set $F\subseteq X$. Since $X$ is {P2}, $F$ is closed, so $F = X$.
+Since $X$ is {P226}, we can find a finite dense set $F\subseteq X$. Since $X$ is {P2}, $F$ is closed, so $F = X$.

From 8df29e31d54997b96b8a677058e4152c07221c94 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 4 Jan 2026 00:35:01 +0100
Subject: [PATCH 30/34] improve indiscrete theorem

---
 theorems/T000823.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/theorems/T000823.md b/theorems/T000823.md
index 3c6885b16..c29ed29d0 100644
--- a/theorems/T000823.md
+++ b/theorems/T000823.md
@@ -1,9 +1,11 @@
 ---
 uid: T000823
 if:
-  P000129: true
+  and:
+  - P000016: true
+  - P000185: true
 then:
   P000226: true
 ---
 
-All collections of open sets are finite.
+The partition generating $X$ must be finite due to $X$ being {P16}. Hence, there can only be finitely many open sets, which trivially implies {P226}.
\ No newline at end of file

From 92b31d61cbffbc8f9723bfbdaf0b9648fab6dc40 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sun, 4 Jan 2026 03:23:43 +0100
Subject: [PATCH 31/34] Update theorems/T000823.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000823.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theorems/T000823.md b/theorems/T000823.md
index c29ed29d0..bc82ceba9 100644
--- a/theorems/T000823.md
+++ b/theorems/T000823.md
@@ -8,4 +8,5 @@ then:
   P000226: true
 ---
 
-The partition generating $X$ must be finite due to $X$ being {P16}. Hence, there can only be finitely many open sets, which trivially implies {P226}.
\ No newline at end of file
+The partition generating the topology must be finite due to $X$ being {P16}.
+Hence, there can only be finitely many open sets, which trivially implies {P226}.
\ No newline at end of file

From 3bdbe9eb7be92b7d7285bec9765a052527003937 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Mon, 5 Jan 2026 01:46:00 +0100
Subject: [PATCH 32/34] Update theorems/T000829.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000829.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theorems/T000829.md b/theorems/T000829.md
index 743d81a66..25357be01 100644
--- a/theorems/T000829.md
+++ b/theorems/T000829.md
@@ -8,4 +8,7 @@ then:
   P000078: true
 ---
 
-Since {P226} is hereditary and {P47} implies {P2} ([explore](https://topology.pi-base.org/spaces?q=47+%2B+not+2)), this follows from {T824}.
+Let $p\in X$ be the dispersion point.
+Then $X\setminus\{p\}$ is {P226} and {P47},
+hence {P78}
+[(Explore)](https://topology.pi-base.org/spaces?q=Totally+disconnected%2BArtinian%2B%7EFinite).

From f1c4ad0ca9ece8a17f44173525c45a0ac48404ab Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Mon, 5 Jan 2026 01:46:32 +0100
Subject: [PATCH 33/34] Update theorems/T000828.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000828.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theorems/T000828.md b/theorems/T000828.md
index f9aadc7f8..6e985ab07 100644
--- a/theorems/T000828.md
+++ b/theorems/T000828.md
@@ -6,4 +6,5 @@ then:
   P000021: true
 ---
 
-Since {P226} is hereditary, this follows from {T42} and {T824}.
+Since {P226} is hereditary, every discrete subset of $X$ is finite
+[(Explore)](https://topology.pi-base.org/spaces?q=Discrete%2BArtinian%2B%7EFinite).

From 1b1a62054ce17de1763b6e0c69fc65ffbc610685 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Mon, 5 Jan 2026 01:47:39 +0100
Subject: [PATCH 34/34] Update theorems/T000827.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000827.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theorems/T000827.md b/theorems/T000827.md
index 4f331a9cc..97faab957 100644
--- a/theorems/T000827.md
+++ b/theorems/T000827.md
@@ -8,4 +8,7 @@ then:
   P000078: true
 ---
 
-Let $p \in X$ be the non-isolated point. Since {P226} is hereditary, the discrete space $X \setminus \{p\}$ (and by extension $X$) must be finite by {T824}.
+Let $p \in X$ be the non-isolated point.
+Then $X\setminus\{p\}$ is {P52} and {P226},
+hence {P78}
+[(Explore)](https://topology.pi-base.org/spaces?q=Discrete%2BArtinian%2B%7EFinite).