Semimetrizable spaces are Gδ, add explicit proof to S61|P33

spaces/S000061/properties/P000033.md

@@ -9,3 +9,16 @@ refs:
 
 Asserted in the General Reference Chart for space #69 in
 {{doi:10.1007/978-1-4612-6290-9_6}}.
+
+Here is a direct proof of this fact:
+
+As stated in the Corollary in {{zb:0066.41001}}, a necessary and sufficient condition for $X$ to be {P33} is that, for any nested sequence of closed sets $F_0 \supseteq F_1 \supseteq \cdots$ such that $\bigcap_{n \in \omega} F_n = \varnothing$, there exist open sets $U_0 \supseteq U_1 \supseteq \cdots$ such that $U_i \supseteq F_i$ for each $i$ and $\bigcap_{n \in \omega} U_n = \varnothing$.
+
+Let $q_0, q_1, \dots$ be a permutation of rational numbers $\mathbb Q$. Define $F_n := \left\{ q_i \mid i > n \right\}$, then $\bigcap_{n \in \omega} F_n = \varnothing$.
+Additionally, $F_n$ is closed because the subspace topology of $\mathbb Q$ is {P52}.
+Moreover, $F_n$ is dense in $\mathbb R$ with respect to its usual topology.
+
+Now, suppose $U_n$ is an open set that contains $F_n$.
+Then, the intersection $U_n \cap (\mathbb R \setminus \mathbb Q)$ is a dense open subset of $\mathbb R \setminus \mathbb Q$ when considered with the subspace topology, which coincides with {S28}.
+
+Since {S28|P64}, $\bigcap_{n \in \omega} U_n \cap (\mathbb R \setminus \mathbb Q) \neq \varnothing$. This implies that {S61} is not {P33}.

spaces/S000062/README.md

@@ -8,7 +8,7 @@ refs:
   - doi: 10.1007/978-1-4612-6290-9 
     name: Counterexamples in Topology
 ---
-If $X = \mathbb{R}$, and if $D$ is a dense subset of the Euclidean space $(X, \tau)$ with a dense compliment, we define $\tau^{\ast}$, the discrete rational extension of $\tau$, to be the topology generated from $\tau$ by adding each point of $D$ as an open set. (Then any subset of $D$ will be open in $\tau^{\ast}$.) The Discrete Rational Extension of $\mathbb{R}$ is the space that results when $D = \mathbb{Q}$.
+If $X = \mathbb{R}$, and if $D$ is a dense subset of the Euclidean space $(X, \tau)$ with a dense complement, we define $\tau^{\ast}$, the discrete rational extension of $\tau$, to be the topology generated from $\tau$ by adding each point of $D$ as an open set. (Then any subset of $D$ will be open in $\tau^{\ast}$.) The Discrete Rational Extension of $\mathbb{R}$ is the space that results when $D = \mathbb{Q}$.
 
 Defined as counterexample #70 ("Discrete Rational Extension of $\mathbb{R}$")
 in {{doi:10.1007/978-1-4612-6290-9}}.

spaces/S000063/README.md

@@ -10,7 +10,7 @@ refs:
   - doi: 10.1090/S0002-9904-1963-10931-3
     name: The product of a normal space and a metric space need not be normal (E. Michael)
 ---
-If $X = \mathbb{R}$, and if $D$ is a dense subset of the Euclidean space $(X, \tau)$ with a dense compliment, we define $\tau^{*}$, the discrete extension of $\tau$, to be the topology generated from $\tau$ by adding each point of $D$ as an open set. (Then any subset of $D$ will be open in $\tau^{*}$.) The Discrete Irrational Extension of $\mathbb{R}$ is the space that results when $D = \mathbb{P}$, the set of irrational numbers.
+If $X = \mathbb{R}$, and if $D$ is a dense subset of the Euclidean space $(X, \tau)$ with a dense complement, we define $\tau^{*}$, the discrete extension of $\tau$, to be the topology generated from $\tau$ by adding each point of $D$ as an open set. (Then any subset of $D$ will be open in $\tau^{*}$.) The Discrete Irrational Extension of $\mathbb{R}$ is the space that results when $D = \mathbb{P}$, the set of irrational numbers.
 
 The use of this space by [Ernest Michael](https://en.wikipedia.org/wiki/Ernest_Michael) in {{doi:10.1090/S0002-9904-1963-10931-3}} resulted in it being known as the "Michael line".  See for example <https://dantopology.wordpress.com/2012/10/28/michael-line-basics/>.
 

theorems/T000699.md

@@ -0,0 +1,16 @@
+---
+uid: T000699
+if:
+  P000102: true
+then:
+  P000132: true
+---
+
+Let $A \subseteq X$ be a closed subset.
+
+For each $x \in X$ and $\varepsilon > 0$, the set $U(x, \varepsilon) := \operatorname{int} B_d(x, \varepsilon)$ is an open neighborhood of $x$.
+Define $G_n := \bigcup_{x \in A} U\!\left( x, \frac 1n \right)$. This is an open set containing $A$.
+
+If $y \notin A$, then there exists some $n \in \omega$ such that $d(y, A) > \frac 1n$. Consequently, $y \notin B_d(x, \frac 1n)$ for any $x \in A$, which implies $y \notin G_n$.
+
+Therefore, $A = \bigcap_{n \in \omega} G_n$.