feat: T_D property and theorems

properties/P000247.md

@@ -0,0 +1,20 @@
+---
+uid: P000247
+name: "$T_D$"
+refs:
+    - doi: 10.1016/S1385-7258(62)50003-6
+      name: Separation Axioms Between T0 and T1 (Aull and Thron, 1962)
+    - doi: 10.1007/978-3-0348-0154-6
+      name: Frames and Locales (Picado and Pultr, 2012)
+---
+
+The derived set of every subset of $X$ is closed.
+
+Equivalently:
+- for every $x$ there is an open neighborhood $U$ of $x$ s.t. $U\setminus \{x\}$ is also open.
+- every point is isolated in its own closure, i.e. for every $x$ there is an open neighborhood $U$ s.t. $U\cap\overline{\{x\}}=\{x\}$
+
+----
+#### Meta-properties
+
+- This property is hereditary.

spaces/S000042/properties/P000247.md

@@ -0,0 +1,11 @@
+---
+space: S000042
+property: P000247
+value: false
+---
+
+For any $y \in X$, the closure $\overline{\{y\}}=\mathbb{R}\setminus B_y = (-\infty, y]$. 
+So consider open $U\ni y$. 
+If $U=\mathbb{R}$ then $U\cap \overline{\{y\}} = (-\infty, y]\neq \{y\}$. 
+If $U=(a,\infty)$ with $a < y$, then $U \cap \overline{\{y\}} = (a,y]\neq \{y\}$ either. 
+So the space cannot be {P247}.

spaces/S000082/properties/P000247.md

@@ -0,0 +1,8 @@
+---
+space: S000082
+property: P000247
+value: false
+---
+
+$X$ contains a copy of {S42} as a subspace,
+and {S42|P247}.

theorems/T000932.md

@@ -0,0 +1,15 @@
+---
+uid: T000932
+if:
+  P000247: true
+then:
+  P000001: true
+refs:
+  - doi: 10.1016/S1385-7258(62)50003-6
+    name: Separation Axioms Between T0 and T1 (Aull and Thron, 1962)
+---
+
+Suppose two distinct points $x,y \in X$ that are topologically indistinguishable, take $U\ni x$ open such that $U\setminus \{x\}$ is open. 
+Then $y\in U$ and $y\in U \setminus \{x\}$, which is an open set containing $y$ but not $x$, which contradicts indistinguishability. Thus $X$ is {P1}.
+
+See also Definition 3.1 in {{zb:0108.35402}}.

theorems/T000933.md

@@ -0,0 +1,14 @@
+---
+uid: T000933
+if:
+  P000002: true
+then:
+  P000247: true
+refs:
+  - doi: 10.1016/S1385-7258(62)50003-6
+    name: Separation Axioms Between T0 and T1 (Aull and Thron, 1962)
+---
+
+The set $\{x\}$ is closed, so for any open neighborhood $U$ of $x$, $U \setminus \{x\} = U \cap X \setminus \{x\}$ is open.
+
+See also Definition 3.1 in {{zb:0108.35402}}.

theorems/T000934.md

@@ -0,0 +1,25 @@
+---
+uid: T000934
+if:
+  and:
+  - P000001: true
+  - P000090: true
+then:
+  P000247: true
+refs:
+  - doi: 10.1016/S1385-7258(62)50003-6
+    name: Separation Axioms Between T0 and T1 (Aull and Thron, 1962)
+---
+
+Let $x\in X$, by {P90} there exists a minimal open neighborhood $U_x$ of $x$.
+Now consider $W=\bigcup\{U_y : y \in U_x, y\neq x\}$, which is open in $X$. 
+
+We claim that $U_x \setminus \{x\} = W$. 
+
+For $\subseteq$: each $y$ lies in $U_y$ which is in $W$. 
+
+For $\supseteq$: if $y \in U_x$ and $x\neq y$, then $U_y \subseteq U_x$, and $x \notin U_y$ since that would contradict minimality of $U_x$ and that by {P1} such minimal open sets are unique to each point.
+
+Hence $U_x \setminus \{x\}$ is open which shows {P247}.
+
+See also Theorem 5.2 in {{zb:0108.35402}}.

theorems/T000935.md

@@ -0,0 +1,13 @@
+---
+uid: T000935
+if:
+  P000051: true
+then:
+  P000247: true
+---
+
+Let $x \in X$ and $C=\overline{\{x\}}\neq\emptyset$. 
+By {P51} some $y\in C$ is isolated, so $U\cap C=\{y\}$ with $U$ open. 
+Thus $U$ meets $\overline{\{x\}}$, so by openness $U$ meets $\{x\}$. 
+
+So $x \in U\cap C = \{y\}$, hence $x=y$ and $U\cap\overline{\{x\}}=\{x\}$, giving {P247}.

theorems/T000936.md

@@ -0,0 +1,13 @@
+---
+uid: T000936
+if:
+  and:
+    - P000201: true
+    - P000247: true
+then:
+  P000139: true
+---
+
+Let $p\in X$ be a generic point so $\overline{\{p\}}=X$. 
+By {P247} there exists an open neighborhood $U$ s.t. $U\cap \overline{\{p\}} = U \cap X= \{p\}$. 
+Then $U=\{p\}$, and $p$ is isolated.