From 1fe7e3b3a95e902501bcdbfa52f0b1c0b16e661c Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Thu, 9 Jul 2026 08:45:50 +0200
Subject: [PATCH 01/13] Add theorems and space from #1800

---
 spaces/S000227/README.md             |  6 ++++++
 spaces/S000227/properties/P000181.md |  7 +++++++
 spaces/S000227/properties/P000245.md |  7 +++++++
 theorems/T000914.md                  | 10 ++++++++++
 theorems/T000915.md                  | 10 ++++++++++
 5 files changed, 40 insertions(+)
 create mode 100644 spaces/S000227/README.md
 create mode 100644 spaces/S000227/properties/P000181.md
 create mode 100644 spaces/S000227/properties/P000245.md
 create mode 100644 theorems/T000914.md
 create mode 100644 theorems/T000915.md

diff --git a/spaces/S000227/README.md b/spaces/S000227/README.md
new file mode 100644
index 000000000..d97ef4878
--- /dev/null
+++ b/spaces/S000227/README.md
@@ -0,0 +1,6 @@
+---
+uid: S000227
+name: Almost indiscrete topology on $\omega$
+---
+
+Let $X=\omega$ with the topology $\tau = \{\emptyset, \{0\}, \infty\}$.
diff --git a/spaces/S000227/properties/P000181.md b/spaces/S000227/properties/P000181.md
new file mode 100644
index 000000000..aa1f9cb15
--- /dev/null
+++ b/spaces/S000227/properties/P000181.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000181
+value: true
+---
+
+By definition.
\ No newline at end of file
diff --git a/spaces/S000227/properties/P000245.md b/spaces/S000227/properties/P000245.md
new file mode 100644
index 000000000..06df0483f
--- /dev/null
+++ b/spaces/S000227/properties/P000245.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000245
+value: true
+---
+
+By definition.
\ No newline at end of file
diff --git a/theorems/T000914.md b/theorems/T000914.md
new file mode 100644
index 000000000..3a3aff2ee
--- /dev/null
+++ b/theorems/T000914.md
@@ -0,0 +1,10 @@
+---
+uid: T000914
+if:
+  and:
+  - P000073: true
+  - P000090: true
+then:
+  P000051: false
+---
+(todo)
diff --git a/theorems/T000915.md b/theorems/T000915.md
new file mode 100644
index 000000000..6b663ce0d
--- /dev/null
+++ b/theorems/T000915.md
@@ -0,0 +1,10 @@
+---
+uid: T000914
+if:
+  and:
+  - P000051: true
+  - P000208: true
+then:
+  P000078: false
+---
+(todo)

From 0e2dde2237717c2c6da0747119d58e481a8bd80a Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Thu, 9 Jul 2026 09:16:07 +0200
Subject: [PATCH 02/13] fix uid

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

diff --git a/theorems/T000915.md b/theorems/T000915.md
index 6b663ce0d..6cd0e59f9 100644
--- a/theorems/T000915.md
+++ b/theorems/T000915.md
@@ -1,5 +1,5 @@
 ---
-uid: T000914
+uid: T000915
 if:
   and:
   - P000051: true

From 933d824a1db2b122b407f3639860161a25766b46 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Sun, 12 Jul 2026 20:23:17 +0200
Subject: [PATCH 03/13] test

---
 theorems/T000915.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theorems/T000915.md b/theorems/T000915.md
index 6cd0e59f9..91731fa66 100644
--- a/theorems/T000915.md
+++ b/theorems/T000915.md
@@ -8,3 +8,4 @@ then:
   P000078: false
 ---
 (todo)
+test commit

From f0bc8a57b5a8d127ee4e4d7e8c37f71b80bde12a Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Mon, 13 Jul 2026 09:09:11 +0200
Subject: [PATCH 04/13] fix theorem

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

diff --git a/theorems/T000914.md b/theorems/T000914.md
index 3a3aff2ee..a05eec4f1 100644
--- a/theorems/T000914.md
+++ b/theorems/T000914.md
@@ -5,6 +5,6 @@ if:
   - P000073: true
   - P000090: true
 then:
-  P000051: false
+  P000051: true
 ---
 (todo)

From b056498af096a27538d5cb2c0e8ba210e163adc4 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Mon, 13 Jul 2026 09:11:28 +0200
Subject: [PATCH 05/13] fix theorem

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

diff --git a/theorems/T000915.md b/theorems/T000915.md
index 91731fa66..3d9a6a25b 100644
--- a/theorems/T000915.md
+++ b/theorems/T000915.md
@@ -5,7 +5,7 @@ if:
   - P000051: true
   - P000208: true
 then:
-  P000078: false
+  P000078: true
 ---
 (todo)
 test commit

From 010fca1f592994c2b428306684ba002da14b058e Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Mon, 13 Jul 2026 09:25:00 +0200
Subject: [PATCH 06/13] quasi-sober + alexandrov + noetherian => has finitely
 many open sets

---
 spaces/S000227/README.md |  2 +-
 theorems/T000916.md      | 12 ++++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 theorems/T000916.md

diff --git a/spaces/S000227/README.md b/spaces/S000227/README.md
index d97ef4878..ecefa4267 100644
--- a/spaces/S000227/README.md
+++ b/spaces/S000227/README.md
@@ -3,4 +3,4 @@ uid: S000227
 name: Almost indiscrete topology on $\omega$
 ---
 
-Let $X=\omega$ with the topology $\tau = \{\emptyset, \{0\}, \infty\}$.
+Let $X=\omega$ with the topology $\tau = \{\emptyset, \{0\}, X\}$.
diff --git a/theorems/T000916.md b/theorems/T000916.md
new file mode 100644
index 000000000..be7760c9e
--- /dev/null
+++ b/theorems/T000916.md
@@ -0,0 +1,12 @@
+---
+uid: T000916
+if:
+  and:
+  - P000192: true
+  - P000090: true
+  - P000208: true
+then:
+  P000245: true
+---
+
+{P73}+{P90}+{P208} is {P78} ([Explore](https://topology.pi-base.org/spaces?q=Sober+%2B+Alexandrov+%2B+Noetherian+%2B+%7EFinite)), so with {P192} we can generalize this by undoing the Kolmogorov quotient, which implies {P245}.

From 6af56c00569ccbb9a7d77ff73f8d44007ff5f278 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Mon, 13 Jul 2026 09:32:13 +0200
Subject: [PATCH 07/13] S227 is not P39 (Hyperconnected)

---
 spaces/S000227/properties/P000039.md | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 spaces/S000227/properties/P000039.md

diff --git a/spaces/S000227/properties/P000039.md b/spaces/S000227/properties/P000039.md
new file mode 100644
index 000000000..38435539d
--- /dev/null
+++ b/spaces/S000227/properties/P000039.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000039
+value: true
+---
+
+By inspection, the only nonempty open sets are $\{0\}$ and $X$ which are not disjoint.

From ddacc7980f3682b703ae7d967110ef18a74ef79d Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Tue, 14 Jul 2026 16:03:33 +0200
Subject: [PATCH 08/13] more basic properties for S227

---
 spaces/S000227/README.md             | 2 +-
 spaces/S000227/properties/P000040.md | 7 +++++++
 spaces/S000227/properties/P000139.md | 7 +++++++
 spaces/S000227/properties/P000201.md | 7 +++++++
 4 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 spaces/S000227/properties/P000040.md
 create mode 100644 spaces/S000227/properties/P000139.md
 create mode 100644 spaces/S000227/properties/P000201.md

diff --git a/spaces/S000227/README.md b/spaces/S000227/README.md
index ecefa4267..2926bac54 100644
--- a/spaces/S000227/README.md
+++ b/spaces/S000227/README.md
@@ -1,6 +1,6 @@
 ---
 uid: S000227
-name: Almost indiscrete topology on $\omega$
+name: $\omega$ with the basis $\{\{0\},X\}$
 ---
 
 Let $X=\omega$ with the topology $\tau = \{\emptyset, \{0\}, X\}$.
diff --git a/spaces/S000227/properties/P000040.md b/spaces/S000227/properties/P000040.md
new file mode 100644
index 000000000..e4c5c6182
--- /dev/null
+++ b/spaces/S000227/properties/P000040.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000040
+value: true
+---
+
+The only closed sets are $X\setminus \{0\}$ and $X$, and they are not disjoint.
\ No newline at end of file
diff --git a/spaces/S000227/properties/P000139.md b/spaces/S000227/properties/P000139.md
new file mode 100644
index 000000000..45a651cc9
--- /dev/null
+++ b/spaces/S000227/properties/P000139.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000139
+value: true
+---
+
+The singleton $\{0\}$ is isolated.
\ No newline at end of file
diff --git a/spaces/S000227/properties/P000201.md b/spaces/S000227/properties/P000201.md
new file mode 100644
index 000000000..65d861d2e
--- /dev/null
+++ b/spaces/S000227/properties/P000201.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000201
+value: true
+---
+
+The point $0$ is a generic point, since $\overline{\{0\}} = X$.
\ No newline at end of file

From 553e36f11f1aaa25ec615219878be135851b9180 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Tue, 14 Jul 2026 16:15:37 +0200
Subject: [PATCH 09/13] S227 is P107, rename S227, newlines, remove redundant
 P39

---
 spaces/S000227/README.md             | 2 +-
 spaces/S000227/properties/P000039.md | 7 -------
 spaces/S000227/properties/P000040.md | 2 +-
 spaces/S000227/properties/P000107.md | 7 +++++++
 spaces/S000227/properties/P000139.md | 2 +-
 spaces/S000227/properties/P000181.md | 2 +-
 spaces/S000227/properties/P000201.md | 2 +-
 spaces/S000227/properties/P000245.md | 2 +-
 8 files changed, 13 insertions(+), 13 deletions(-)
 delete mode 100644 spaces/S000227/properties/P000039.md
 create mode 100644 spaces/S000227/properties/P000107.md

diff --git a/spaces/S000227/README.md b/spaces/S000227/README.md
index 2926bac54..675ef011d 100644
--- a/spaces/S000227/README.md
+++ b/spaces/S000227/README.md
@@ -1,6 +1,6 @@
 ---
 uid: S000227
-name: $\omega$ with the basis $\{\{0\},X\}$
+name: Countable set with the basis $\{\{0\},X\}$
 ---
 
 Let $X=\omega$ with the topology $\tau = \{\emptyset, \{0\}, X\}$.
diff --git a/spaces/S000227/properties/P000039.md b/spaces/S000227/properties/P000039.md
deleted file mode 100644
index 38435539d..000000000
--- a/spaces/S000227/properties/P000039.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000039
-value: true
----
-
-By inspection, the only nonempty open sets are $\{0\}$ and $X$ which are not disjoint.
diff --git a/spaces/S000227/properties/P000040.md b/spaces/S000227/properties/P000040.md
index e4c5c6182..a3948b0e1 100644
--- a/spaces/S000227/properties/P000040.md
+++ b/spaces/S000227/properties/P000040.md
@@ -4,4 +4,4 @@ property: P000040
 value: true
 ---
 
-The only closed sets are $X\setminus \{0\}$ and $X$, and they are not disjoint.
\ No newline at end of file
+The only closed sets are $X\setminus \{0\}$ and $X$, and they are not disjoint.
diff --git a/spaces/S000227/properties/P000107.md b/spaces/S000227/properties/P000107.md
new file mode 100644
index 000000000..59dce0543
--- /dev/null
+++ b/spaces/S000227/properties/P000107.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000107
+value: false
+---
+
+The only closed sets are $X\setminus \{0\}$ and $X$, and neither is a point.
diff --git a/spaces/S000227/properties/P000139.md b/spaces/S000227/properties/P000139.md
index 45a651cc9..b9fbf0bc2 100644
--- a/spaces/S000227/properties/P000139.md
+++ b/spaces/S000227/properties/P000139.md
@@ -4,4 +4,4 @@ property: P000139
 value: true
 ---
 
-The singleton $\{0\}$ is isolated.
\ No newline at end of file
+The singleton $\{0\}$ is isolated.
diff --git a/spaces/S000227/properties/P000181.md b/spaces/S000227/properties/P000181.md
index aa1f9cb15..8dd2b4619 100644
--- a/spaces/S000227/properties/P000181.md
+++ b/spaces/S000227/properties/P000181.md
@@ -4,4 +4,4 @@ property: P000181
 value: true
 ---
 
-By definition.
\ No newline at end of file
+By definition.
diff --git a/spaces/S000227/properties/P000201.md b/spaces/S000227/properties/P000201.md
index 65d861d2e..d8271fe81 100644
--- a/spaces/S000227/properties/P000201.md
+++ b/spaces/S000227/properties/P000201.md
@@ -4,4 +4,4 @@ property: P000201
 value: true
 ---
 
-The point $0$ is a generic point, since $\overline{\{0\}} = X$.
\ No newline at end of file
+The point $0$ is a generic point, since $\overline{\{0\}} = X$.
diff --git a/spaces/S000227/properties/P000245.md b/spaces/S000227/properties/P000245.md
index 06df0483f..bedeca38f 100644
--- a/spaces/S000227/properties/P000245.md
+++ b/spaces/S000227/properties/P000245.md
@@ -4,4 +4,4 @@ property: P000245
 value: true
 ---
 
-By definition.
\ No newline at end of file
+By definition.

From 2dd2c2b6f9aa9a4d704294d0f51a0d556d37f495 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Tue, 14 Jul 2026 16:20:14 +0200
Subject: [PATCH 10/13] S227 is P196

---
 spaces/S000227/properties/P000196.md | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 spaces/S000227/properties/P000196.md

diff --git a/spaces/S000227/properties/P000196.md b/spaces/S000227/properties/P000196.md
new file mode 100644
index 000000000..1bb0bb927
--- /dev/null
+++ b/spaces/S000227/properties/P000196.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000196
+value: true
+---
+
+The open sets are ordered by inclusion: $\emptyset \subseteq \{0\} \subseteq X$.
\ No newline at end of file

From c343cfaa654e70d41e8bd7ed476870e722bf2903 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Tue, 14 Jul 2026 17:46:11 +0200
Subject: [PATCH 11/13] S227 is not Toronto

---
 spaces/S000227/properties/P000219.md | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 spaces/S000227/properties/P000219.md

diff --git a/spaces/S000227/properties/P000219.md b/spaces/S000227/properties/P000219.md
new file mode 100644
index 000000000..27cc09886
--- /dev/null
+++ b/spaces/S000227/properties/P000219.md
@@ -0,0 +1,7 @@
+---
+space: S000227
+property: P000219
+value: false
+---
+
+$|X\setminus\{0\}|=|X|$ but $X\setminus\{0\}$ is homeomorphic to {S193} which is {P129}, while {S227|P129}.
\ No newline at end of file

From ceaaeff0e3d4c182a1bf4964260a8103540bc695 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Wed, 15 Jul 2026 12:10:00 +0200
Subject: [PATCH 12/13] nicer wording

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

diff --git a/theorems/T000916.md b/theorems/T000916.md
index be7760c9e..507ee2616 100644
--- a/theorems/T000916.md
+++ b/theorems/T000916.md
@@ -9,4 +9,4 @@ then:
   P000245: true
 ---
 
-{P73}+{P90}+{P208} is {P78} ([Explore](https://topology.pi-base.org/spaces?q=Sober+%2B+Alexandrov+%2B+Noetherian+%2B+%7EFinite)), so with {P192} we can generalize this by undoing the Kolmogorov quotient, which implies {P245}.
+{T914} and {T915}, so by undoing Kolmogorov quotients we can generalize this to {P192} instead of {P73}, which implies {P245} instead of {P78}.

From 6c5765ae08a6ef5d6cd4dc7c6e0c81259ac2e2b5 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Wed, 15 Jul 2026 12:11:25 +0200
Subject: [PATCH 13/13] remove s227

---
 spaces/S000227/README.md             | 6 ------
 spaces/S000227/properties/P000040.md | 7 -------
 spaces/S000227/properties/P000107.md | 7 -------
 spaces/S000227/properties/P000139.md | 7 -------
 spaces/S000227/properties/P000181.md | 7 -------
 spaces/S000227/properties/P000196.md | 7 -------
 spaces/S000227/properties/P000201.md | 7 -------
 spaces/S000227/properties/P000219.md | 7 -------
 spaces/S000227/properties/P000245.md | 7 -------
 9 files changed, 62 deletions(-)
 delete mode 100644 spaces/S000227/README.md
 delete mode 100644 spaces/S000227/properties/P000040.md
 delete mode 100644 spaces/S000227/properties/P000107.md
 delete mode 100644 spaces/S000227/properties/P000139.md
 delete mode 100644 spaces/S000227/properties/P000181.md
 delete mode 100644 spaces/S000227/properties/P000196.md
 delete mode 100644 spaces/S000227/properties/P000201.md
 delete mode 100644 spaces/S000227/properties/P000219.md
 delete mode 100644 spaces/S000227/properties/P000245.md

diff --git a/spaces/S000227/README.md b/spaces/S000227/README.md
deleted file mode 100644
index 675ef011d..000000000
--- a/spaces/S000227/README.md
+++ /dev/null
@@ -1,6 +0,0 @@
----
-uid: S000227
-name: Countable set with the basis $\{\{0\},X\}$
----
-
-Let $X=\omega$ with the topology $\tau = \{\emptyset, \{0\}, X\}$.
diff --git a/spaces/S000227/properties/P000040.md b/spaces/S000227/properties/P000040.md
deleted file mode 100644
index a3948b0e1..000000000
--- a/spaces/S000227/properties/P000040.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000040
-value: true
----
-
-The only closed sets are $X\setminus \{0\}$ and $X$, and they are not disjoint.
diff --git a/spaces/S000227/properties/P000107.md b/spaces/S000227/properties/P000107.md
deleted file mode 100644
index 59dce0543..000000000
--- a/spaces/S000227/properties/P000107.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000107
-value: false
----
-
-The only closed sets are $X\setminus \{0\}$ and $X$, and neither is a point.
diff --git a/spaces/S000227/properties/P000139.md b/spaces/S000227/properties/P000139.md
deleted file mode 100644
index b9fbf0bc2..000000000
--- a/spaces/S000227/properties/P000139.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000139
-value: true
----
-
-The singleton $\{0\}$ is isolated.
diff --git a/spaces/S000227/properties/P000181.md b/spaces/S000227/properties/P000181.md
deleted file mode 100644
index 8dd2b4619..000000000
--- a/spaces/S000227/properties/P000181.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000181
-value: true
----
-
-By definition.
diff --git a/spaces/S000227/properties/P000196.md b/spaces/S000227/properties/P000196.md
deleted file mode 100644
index 1bb0bb927..000000000
--- a/spaces/S000227/properties/P000196.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000196
-value: true
----
-
-The open sets are ordered by inclusion: $\emptyset \subseteq \{0\} \subseteq X$.
\ No newline at end of file
diff --git a/spaces/S000227/properties/P000201.md b/spaces/S000227/properties/P000201.md
deleted file mode 100644
index d8271fe81..000000000
--- a/spaces/S000227/properties/P000201.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000201
-value: true
----
-
-The point $0$ is a generic point, since $\overline{\{0\}} = X$.
diff --git a/spaces/S000227/properties/P000219.md b/spaces/S000227/properties/P000219.md
deleted file mode 100644
index 27cc09886..000000000
--- a/spaces/S000227/properties/P000219.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000219
-value: false
----
-
-$|X\setminus\{0\}|=|X|$ but $X\setminus\{0\}$ is homeomorphic to {S193} which is {P129}, while {S227|P129}.
\ No newline at end of file
diff --git a/spaces/S000227/properties/P000245.md b/spaces/S000227/properties/P000245.md
deleted file mode 100644
index bedeca38f..000000000
--- a/spaces/S000227/properties/P000245.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000227
-property: P000245
-value: true
----
-
-By definition.