Property: Open connected components (#1669)

Author: felixpernegger

properties/P000233.md

@@ -20,9 +20,11 @@ This is equivalent to each of the following:
 
 The equivalence between the various conditions can be shown by arguments similar to those used in the definition of {P42}, in particular {{mathse:3002235}}.
 
-This property is used in the literature, but usually without a separate name. One exception is {{zb:0451.54017}}, where it is called "PCGS" (path connected generated space).
+This property is used in the literature, but usually without a separate name.
+One exception is {{zb:0451.54017}} (accessible [here](https://topology.nipissingu.ca/tp/reprints/v04/tp04204.pdf)),
+where it is called "PCGS" (path connectedly generated space).
 
-Compare with {P42}.
+Compare with {P42} and {P234}.
 
 ----
 #### Meta-properties

properties/P000234.md

@@ -0,0 +1,35 @@
+---
+uid: P000234
+name: Has open connected components
+refs:
+  - mathse: 3002235
+    name: Answer to "Definition of locally pathwise connected"
+  - zb: "0451.54017"
+    name: Topologies determined by paths (S. Franklin, B. Smith-Thomas)
+---
+
+Every connected component of $X$ is open.
+
+This is equivalent to each of the following:
+
+* Each point $x\in X$ has a connected neighborhood.
+
+* Each point $x\in X$ has an open connected neighborhood.
+
+* $X$ is a topological disjoint union of {P36} spaces.
+
+The equivalence between the various conditions can be shown by arguments similar to those used in the definition of {P42}, in particular {{mathse:3002235}}.
+
+This property is normally used without a separate name. But see {{zb:0451.54017}}
+(accessible [here](https://topology.nipissingu.ca/tp/reprints/v04/tp04204.pdf)),
+where it is called "CGS" (connectedly generated space).
+
+Compare with {P41} and {P233}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
+- This property is hereditary with respect to clopen sets.
+- This property is preserved by finite products.
+- This property is preserved by arbitrary disjoint unions.

theorems/T000108.md

@@ -2,15 +2,11 @@
 uid: T000108
 if:
   and:
+  - P000234: true
   - P000047: true
-  - P000041: true
 then:
   P000052: true
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
 ---
 
-If every point has a connected neighborhood and the only connected sets are single points, then every point has a neighborhood consisting of the point itself.
-
-Proven on page 32 of {{zb:0386.54001}}.
+By {P47} the connected components of $X$ are singletons,
+so by {P234} every singleton is open.

theorems/T000862.md

@@ -0,0 +1,9 @@
+---
+uid: T000862
+if:
+  P000233: true
+then:
+  P000234: true
+---
+
+Immediate from the (equivalent) definitions using {T40}.

theorems/T000863.md

@@ -0,0 +1,9 @@
+---
+uid: T000863
+if:
+  P000041: true
+then:
+  P000234: true
+---
+
+Immediate from the definitions.

theorems/T000864.md

@@ -0,0 +1,9 @@
+---
+uid: T000864
+if:
+  P000036: true
+then:
+  P000234: true
+---
+
+Immediate from the definitions.