implement suggestions and add new theorems

properties/P000185.md

@@ -2,8 +2,10 @@
 uid: P000185
 name: Partition topology
 refs:
- - doi: 10.1007/978-1-4612-6290-9
- name: Counterexamples in Topology
+- doi: 10.1007/978-1-4612-6290-9
+ name: Counterexamples in Topology
+- doi: 10.5186/aasfm.1977.0321
+ name: On ultrapseudocompact and related spaces (T. Nieminen)
 ---
 
 Any of the following equivalent properties holds:
@@ -14,7 +16,7 @@ Any of the following equivalent properties holds:
 - The space's Kolmogorov quotient is {P52}.
 - The space is the disjoint union of a collection of {P129} spaces.
 
-For further characterizations, see theorem 25 of https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf.
+For proof of the equivalences and further characterizations, see section 13 of {{doi:10.5186/aasfm.1977.0321}}.
 
 Defined as example #5 ("Partition Topology")
 in {{doi:10.1007/978-1-4612-6290-9}}.

properties/P000196.md

@@ -4,14 +4,15 @@ name: Hereditarily connected
 aliases:
 - Totally ordered topology
 refs:
-- zb: "0396.54009"
+- doi: 10.5186/aasfm.1977.0321
  name: On ultrapseudocompact and related spaces (T. Nieminen)
 ---
 
 Any of the following equivalent properties holds:
 
 - Any subspace is connected.
-- The open sets are totally ordered by set inclusion.
+- The open sets are totally ordered by inclusion.
+- The closed sets are totally ordered by inclusion.
 - The specialization preorder is total.
 
-For further characterizations, see theorem 22 of https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf.
+For proof of the equivalences and further characterizations, see section 12 of {{doi:10.5186/aasfm.1977.0321}}.

theorems/T000547.md

@@ -6,4 +6,4 @@ then:
  P000014: true
 ---
 
-Any {P196} space is trivially {P13} (as there are no disoint closed sets), and the property is hereditary, so all subspaces are as well.
+Any {P196} space is trivially {P13} (as there are no disjoint closed sets), so all subspaces are as well.

theorems/T000548.md

@@ -7,8 +7,8 @@ if:
 then:
  P000196: true
 refs:
-- zb: "0396.54009"
+- doi: 10.5186/aasfm.1977.0321
  name: On ultrapseudocompact and related spaces (T. Nieminen)
 ---
 
-See theorem 23 at https://www.acadsci.fi/mathematica/Vol03/vol03pp185-205.pdf (reading $T_5$ as {P14}).
+See condition (10) of theorem 23 at {{doi:10.5186/aasfm.1977.0321}} (reading $T_5$ as {P14}).

theorems/T000549.md

@@ -6,4 +6,4 @@ then:
  P000174: true
 ---
 
-The topology is totally ordered by set inclusion, so the set of open neighborhoods of any point is as well.
+The topology is totally ordered by inclusion, so the set of open neighborhoods of any point is as well.

theorems/T000550.md

@@ -2,10 +2,10 @@
 uid: T000550
 if:
  and:
- - P000196: true
- - P000057: true
+ - P000193: true
+ - P000039: true
 then:
- P000027: true
+ P000146: true
 ---
 
-There can be no more open sets in a {P196} space than there are points.
+In a {P39} space $X$, every nonempty open set is dense, so to admit a shrinking, every open cover must contain $X$. Thus, any open cover admits a clopen refinement.

theorems/T000555.md

@@ -7,5 +7,4 @@ if:
 then:
  P000044: false
 ---
-
-Since any subset is connected, any partition into non-singletons suffices.
+$X$ has two disjoint subsets, each with at least two points, and each of the subsets is connected.

theorems/T000556.md

@@ -2,11 +2,9 @@
 uid: T000556
 if:
  and:
- - P000196: true
- - P000016: true
+ - P000146: true
+ - P000036: true
 then:
- P000146: true
+ P000016: 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.
+Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, $\{X\}$ is a finite subcover.

theorems/T000558.md

@@ -0,0 +1,10 @@
+---
+uid: T000558
+if:
+ and:
+ - P000146: true
+ - P000036: true
+then:
+ P000020: true
+---
+Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so any sequence converges to all points outside of that union (whose only neighborhood is $X$).

theorems/T000559.md

@@ -0,0 +1,8 @@
+---
+uid: T000558
+if:
+ P000040: true
+then:
+ P000088: true
+---
+In an {P40} space, since any two nonempty closed sets intersect, any discrete family of closed sets can only contain one nonempty set (which is contained in the open set $X$).