Sequentially discrete implies $\alpha_1$ (#1432)

Author: Moniker1998

theorems/T000784.md

@@ -0,0 +1,9 @@
+---
+uid: T000784
+if:
+  P000167: true
+then:
+  P000210: true
+---
+
+Since $X$ has no injective convergent sequences, it is vacuously {P210}.

theorems/T000785.md

@@ -0,0 +1,10 @@
+---
+uid: T000785
+if:
+  P000136: true
+then:
+  P000210: true
+---
+
+If $A$ is an injective convergent sequence with limit $x$, then $A\cup \{x\}$ is infinite and compact.
+Since $X$ has no infinite compact subset, it has no injective convergent sequence, so it is vacuously {P210}.