Property: Path components are open (#1662)

Author: felixpernegger

properties/P000233.md

@@ -0,0 +1,33 @@
+---
+uid: P000233
+name: Has open path components
+refs:
+  - zb: "0451.54017"
+    name: Topologies determined by paths (S. Franklin, B. Smith-Thomas)
+  - mathse: 3002235
+    name: Answer to "Definition of locally pathwise connected"
+---
+
+Every path component of $X$ is open.
+
+This is equivalent to each of the following:
+
+* Each point $x\in X$ has a path connected neighborhood.
+
+* Each point $x\in X$ has an open path connected neighborhood.
+
+* $X$ is a topological disjoint union of {P37} 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 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).
+
+Compare with {P42}.
+
+----
+#### 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/T000089.md

@@ -2,14 +2,11 @@
 uid: T000089
 if:
   and:
-  - P000042: true
-  - P000052: false
+  - P000233: true
+  - P000046: true
 then:
-  P000046: false
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
+  P000052: true
 ---
 
-If a point of $X$ has a non-trivial path connected neighborhood, then $X$ is not totally path disconnected.
-See the discussion on page 32 of {{zb:0386.54001}}.
+By {P46} the path components of $X$ are singletons, 
+so by {P233} every singleton is open.

theorems/T000095.md

@@ -3,14 +3,9 @@ uid: T000095
 if:
   and:
   - P000036: true
-  - P000042: true
+  - P000233: true
 then:
   P000037: true
-refs:
-- zb: "1052.54001"
-  name: General Topology (Willard)
 ---
 
-If $X$ is locally path connected, then since the concatenation of two paths is again a path, path components are both open and closed.
-
-See Theorem 27.5 of {{zb:1052.54001}}.
+All path components of $X$ are open, hence also clopen.

theorems/T000859.md

@@ -0,0 +1,9 @@
+---
+uid: T000859
+if:
+  P000231: true
+then:
+  P000233: true
+---
+
+Immediate from the definitions, since {T590}.

theorems/T000860.md

@@ -0,0 +1,9 @@
+---
+uid: T000860
+if:
+  P000037: true
+then:
+  P000233: true
+---
+
+Immediate from the definitions.

theorems/T000861.md

@@ -0,0 +1,9 @@
+---
+uid: T000861
+if:
+  P000042: true
+then:
+  P000233: true
+---
+
+Immediate from the definitions.