From 3c78e80e32638ab5915f7e27eb06264355c17f4b Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Wed, 22 Jan 2025 18:43:21 -0500
Subject: [PATCH] P85: Basically disconnected (#1206)

---
 properties/P000049.md | 12 ++++++++++--
 properties/P000085.md | 18 ++++++++++++++++++
 theorems/T000673.md   |  9 ++++-----
 theorems/T000693.md   | 12 ++++++++++++
 theorems/T000694.md   | 11 +++++++++++
 theorems/T000695.md   | 15 +++++++++++++++
 theorems/T000696.md   |  9 +++++++++
 theorems/T000697.md   | 14 ++++++++++++++
 8 files changed, 93 insertions(+), 7 deletions(-)
 create mode 100644 properties/P000085.md
 create mode 100644 theorems/T000693.md
 create mode 100644 theorems/T000694.md
 create mode 100644 theorems/T000695.md
 create mode 100644 theorems/T000696.md
 create mode 100644 theorems/T000697.md

diff --git a/properties/P000049.md b/properties/P000049.md
index 20e210cb89..f655d65b4c 100644
--- a/properties/P000049.md
+++ b/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}}).
diff --git a/properties/P000085.md b/properties/P000085.md
new file mode 100644
index 0000000000..d5c75a4ea0
--- /dev/null
+++ b/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.
diff --git a/theorems/T000673.md b/theorems/T000673.md
index 272d9f53cf..42021eaa02 100644
--- a/theorems/T000673.md
+++ b/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$.
diff --git a/theorems/T000693.md b/theorems/T000693.md
new file mode 100644
index 0000000000..60daa262a3
--- /dev/null
+++ b/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.
diff --git a/theorems/T000694.md b/theorems/T000694.md
new file mode 100644
index 0000000000..9202abb4c8
--- /dev/null
+++ b/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.
diff --git a/theorems/T000695.md b/theorems/T000695.md
new file mode 100644
index 0000000000..ddd7ae9142
--- /dev/null
+++ b/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}}.
diff --git a/theorems/T000696.md b/theorems/T000696.md
new file mode 100644
index 0000000000..6e051d8fe6
--- /dev/null
+++ b/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.
diff --git a/theorems/T000697.md b/theorems/T000697.md
new file mode 100644
index 0000000000..46559069ef
--- /dev/null
+++ b/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$.