multiple more theorems

theorems/T000552.md

@@ -8,7 +8,6 @@ if:
 then:
  P000129: true
 ---
-
 If a {P196} space is {P16}, then it must have a second largest open set 
 (otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover).
 To be {P86}, no points can lie in this second-largest set, so the space is {P129}.

theorems/T000553.md

@@ -1,14 +1,9 @@
 ---
 uid: T000553
 if:
- and:
- - P000001: true
- - P000090: true
- - P000027: true
+ P000196: true
 then:
- P000057: true
+ P000042: true
 ---
 
-In an {P90} space, the smallest basis is the set of smallest neighborhoods of points.
-When it is also {P1}, these are all distinct, so they are in bijection with the set of points.
-Thus, such a space has a countable basis iff it is countable.
+Every subset of a {P196} space is {P40}, and {T38}.

theorems/T000554.md

@@ -12,4 +12,4 @@ refs:
 - doi: 10.1017/9781316543870
  name: Spectral spaces (Dickmann, Schwartz, Tressl)
 ---
-Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}.
+Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. In particular, it follows that the specialization order is order-isomorphic to a non-limit ordinal.

theorems/T000555.md

@@ -0,0 +1,11 @@
+---
+uid: T000555
+if:
+ and:
+ - P000196: true
+ - P000176: true
+then:
+ P000044: false
+---
+
+Since any subset is connected, any partition into non-singletons suffices.

theorems/T000556.md

@@ -0,0 +1,12 @@
+---
+uid: T000556
+if:
+ and:
+ - P000196: true
+ - P000016: true
+then:
+ P000146: true
+---
+If a {P196} space is {P16}, then it must have a second largest open set 
+(otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover).
+Thus, any open cover must contain $X$, so it admits a refinement containing $X$ as the only nonempty set.

theorems/T000557.md

@@ -0,0 +1,14 @@
+---
+uid: T000557
+if:
+ and:
+ - P000001: true
+ - P000090: true
+ - P000027: true
+then:
+ P000057: true
+---
+
+In an {P90} space, the smallest basis is the set of smallest neighborhoods of points.
+When it is also {P1}, these are all distinct, so they are in bijection with the set of points.
+Thus, such a space has a countable basis iff it is countable.