Toronto ordinals are discrete (#1802)

Author: artemetra

theorems/T000907.md

@@ -0,0 +1,15 @@
+---
+uid: T000907
+if:
+  and:
+  - P000190: true
+  - P000219: true
+then:
+  P000052: true
+---
+
+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.