From b13ff58aec5049f659a5354122925d487c5fa2b3 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Fri, 12 Jun 2026 12:38:23 +0200
Subject: [PATCH 1/4] Toronto ordinals are discrete

---
 theorems/T000907.md | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 theorems/T000907.md

diff --git a/theorems/T000907.md b/theorems/T000907.md
new file mode 100644
index 000000000..42ed2eb1e
--- /dev/null
+++ b/theorems/T000907.md
@@ -0,0 +1,11 @@
+---
+uid: T000907
+if:
+  and:
+  - P000190: true
+  - P000219: true
+then:
+  P000052: true
+---
+
+If $X$ is finite, then its automatically discrete ([Explore](https://topology.pi-base.org/spaces?q=Finite+%2B+Ordinal+space+%2B+%7EDiscrete)). Thus take $X\geq \omega$ to be infinite, then consider the subset $S=\{\beta + 1 : \beta +1 < X\}$ of successor ordinals lesser than $X$. Every point in $S$ is isolated, hence $S$ is discrete, hence by the fact that $|S|=|X|$ and Toronto, $X$ is discrete as well.

From bca630dacfd79549ffeb3a0788cba4c76a6f931b Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Sun, 14 Jun 2026 09:42:34 +0200
Subject: [PATCH 2/4] typo

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

diff --git a/theorems/T000907.md b/theorems/T000907.md
index 42ed2eb1e..8320ea2ee 100644
--- a/theorems/T000907.md
+++ b/theorems/T000907.md
@@ -8,4 +8,4 @@ then:
   P000052: true
 ---
 
-If $X$ is finite, then its automatically discrete ([Explore](https://topology.pi-base.org/spaces?q=Finite+%2B+Ordinal+space+%2B+%7EDiscrete)). Thus take $X\geq \omega$ to be infinite, then consider the subset $S=\{\beta + 1 : \beta +1 < X\}$ of successor ordinals lesser than $X$. Every point in $S$ is isolated, hence $S$ is discrete, hence by the fact that $|S|=|X|$ and Toronto, $X$ is discrete as well.
+If $X$ is finite, then it's automatically discrete ([Explore](https://topology.pi-base.org/spaces?q=Finite+%2B+Ordinal+space+%2B+%7EDiscrete)). Thus take $X\geq \omega$ to be infinite, then consider the subset $S=\{\beta + 1 : \beta +1 < X\}$ of successor ordinals lesser than $X$. Every point in $S$ is isolated, hence $S$ is discrete, hence by the fact that $|S|=|X|$ and Toronto, $X$ is discrete as well.

From aadbf00e0afb71b301c52a80bf898ee19e97fe67 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Sun, 14 Jun 2026 18:24:28 +0200
Subject: [PATCH 3/4] remove dependency on explore

---
 theorems/T000907.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theorems/T000907.md b/theorems/T000907.md
index 8320ea2ee..1dfa3b39e 100644
--- a/theorems/T000907.md
+++ b/theorems/T000907.md
@@ -8,4 +8,6 @@ then:
   P000052: true
 ---
 
-If $X$ is finite, then it's automatically discrete ([Explore](https://topology.pi-base.org/spaces?q=Finite+%2B+Ordinal+space+%2B+%7EDiscrete)). Thus take $X\geq \omega$ to be infinite, then consider the subset $S=\{\beta + 1 : \beta +1 < X\}$ of successor ordinals lesser than $X$. Every point in $S$ is isolated, hence $S$ is discrete, hence by the fact that $|S|=|X|$ and Toronto, $X$ is discrete as well.
+If $X$ is empty, this holds trivially. Otherwise, take $S=\{0\} \cup \{\beta + 1 : \beta +1 < X\} \subseteq X$ to be the set of $0$ with all successor ordinals less than $X$. Every point in $S$ is isolated, hence $S$ is discrete. 
+For finite $X$ we have that $S=X$ so $X$ is discrete. 
+For infinite $X$, the map $\beta \mapsto \beta+1$ is an injection into $S$, hence $|S|=|X|$ and by Toronto, $X$ is discrete as well.

From 09a6552c8f264a74e36e2b54c9548ae53a354bdd Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Sun, 14 Jun 2026 22:27:15 +0200
Subject: [PATCH 4/4] Update theorems/T000907.md

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

diff --git a/theorems/T000907.md b/theorems/T000907.md
index 1dfa3b39e..49bd23acb 100644
--- a/theorems/T000907.md
+++ b/theorems/T000907.md
@@ -8,6 +8,8 @@ then:
   P000052: true
 ---
 
-If $X$ is empty, this holds trivially. Otherwise, take $S=\{0\} \cup \{\beta + 1 : \beta +1 < X\} \subseteq X$ to be the set of $0$ with all successor ordinals less than $X$. Every point in $S$ is isolated, hence $S$ is discrete. 
-For finite $X$ we have that $S=X$ so $X$ is discrete. 
-For infinite $X$, the map $\beta \mapsto \beta+1$ is an injection into $S$, hence $|S|=|X|$ and by Toronto, $X$ is discrete as well.
+Finite ordinal spaces are discrete.
+So assume $X$ is an infinite ordinal $\alpha$.
+Let $S=\{\beta + 1 : \beta +1 < \alpha\} \subseteq X$ be the set of successor ordinals less than $\alpha$.
+Every point in $S$ is isolated, hence $S$ is discrete.
+The map $\beta \mapsto \beta+1$ is an injection into $S$, hence $|S|=|X|$ and by Toronto, $X$ is discrete as well.