P85: Basically disconnected (#1206)

properties/P000049.md

@@ -8,12 +8,20 @@ refs:
     name: Rings of Continuous Functions (Gillman & Jerison)
   - doi: 10.1007/978-1-4612-6290-9
     name: Counterexamples in Topology
+  - mathse: 3769214
+    name: Dense Subspace of Extremally Disconnected Space is Extremally Disconnected
 ---
 
-A space in which the closure of every open set is open.
+The closure of every open set in $X$ is open (hence clopen).
 
-Equivalently, a space in which any two disjoint open sets have disjoint closures.
+Equivalently, any two disjoint open sets have disjoint closures.
 
 Defined in problem 15G of {{zb:1052.54001}} and problem 1H of {{doi:10.1007/978-1-4615-7819-2}}.
 
 {{doi:1007/978-1-4612-6290-9}} defines it on page 32 with the additional assumption of {P3}, which we do not assume here.
+
+----
+#### Meta-properties
+
+- This property is hereditary with respect to open sets (see Problem 15G.2 in {{zb:1052.54001}}).
+- This property is hereditary with respect to dense sets (see {{mathse:3769214}}).

properties/P000085.md

@@ -0,0 +1,18 @@
+---
+uid: P000085
+name: Basically disconnected
+refs:
+  - doi: 10.1007/978-1-4615-7819-2
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+The closure of every cozero set in $X$ is open (hence clopen).
+
+A *cozero set* is a set of the form $\{x\in X:f(x)>0\}$ for some continuous function $f:X\to\mathbb R$;
+equivalently, the complement of a zero set.
+
+Equivalently, any two disjoint open sets, at least one of which is a cozero set, have disjoint closures.
+
+Defined in problem 1H of {{doi:10.1007/978-1-4615-7819-2}}.
+
+No additional separation axiom is assumed here.

theorems/T000673.md

@@ -2,13 +2,12 @@
 uid: T000673
 if:
   and:
-  - P000147: true
+  - P000085: true
   - P000006: true
 then:
   P000061: true
 ---
 
-Every clopen set in a topological space is a cozero set.
-On the other hand, if $X$ is {P147}, since every zero set is an intersection of countably many open sets, every zero set is clopen, and so is every cozero set.
-So given a cozero set $U$ in $X$, its complement $X\setminus U$ is also a cozero set,
-and their union is obviously dense in $X$.
+Suppose $X$ satisfies the hypotheses.  Then $X$ is {P6}.
+And if $U$ is a cozero set, its closure $\overline U$ is clopen, as is $X\setminus\overline U$.
+So $U$ and $X\setminus\overline U$ are disjoint cozero sets who union is dense in $X$.

theorems/T000693.md

@@ -0,0 +1,12 @@
+---
+uid: T000693
+if:
+  P000049: true
+then:
+  P000085: true
+refs:
+- doi: 10.1007/978-1-4612-6290-9
+  name: Counterexamples in Topology
+---
+
+Evident, as every cozero set is an open set.

theorems/T000694.md

@@ -0,0 +1,11 @@
+---
+uid: T000694
+if:
+  and:
+  - P000085: true
+  - P000015: true
+then:
+  P000049: true
+---
+
+Follows from the definitions since in a {P15} space open sets are cozero sets.

theorems/T000695.md

@@ -0,0 +1,15 @@
+---
+uid: T000695
+if:
+  P000147: true
+then:
+  P000085: true
+refs:
+- zb: "1059.54001"
+  name: Encyclopedia of general topology (Hart et al)
+---
+
+Every cozero set is open and an $F_\sigma$ set, which is closed in a {P147}.
+Hence every cozero set is clopen and its closure is open.
+
+See Figure 1 on page 346 of {{zb:1059.54001}}.

theorems/T000696.md

@@ -0,0 +1,9 @@
+---
+uid: T000696
+if:
+  P000060: true
+then:
+  P000085: true
+---
+
+If $X$ is {P60}, the only cozero sets are $\emptyset$ and $X$, which are clopen.

theorems/T000697.md

@@ -0,0 +1,14 @@
+---
+uid: T000697
+if:
+  and:
+  - P000085: true
+  - P000012: true
+then:
+  P000050: true
+---
+
+Suppose $X$ satisfies the hypotheses.
+Given an open neighborhood $U$ of a point $p$, there is a continuous map $f:X\to[0,1]$ such that $f(p)=0$ and $f(x)=1$ outside of $U$.
+The set $V=\{x\in X:f(x)<1/2\}$ is a cozero set with $p\in V\subseteq\overline V\subseteq U$.
+Its closure $\overline V$ is a clopen neighborhood of $p$ contained in $U$.