Added Banach-Mazur.

src/topology/dst/zero.tex

@@ -22,6 +22,17 @@
     Let $2 = \bracs{0, 1}$ be equipped with the discrete topology, then $2^{\natp}$ is the \textbf{Cantor space}. 
 \end{definition}
 
+\begin{proposition}
+\label{proposition:cantor-space-embedding}
+    The mapping
+    \[
+    2^{\natp} \to [0, 1] \quad \seq{x_n} \mapsto 2\sum_{n \in \natp} \frac{x_n}{3^n}
+    \]
+
+    is an embedding. 
+\end{proposition}
+
+
 \begin{definition}[Baire Space]
 \label{definition:the-baire-space}
     Let $\natp$ be equipped with the discrete topology, then $\mathscr{N} = (\natp)^{\natp}$ is the \textbf{Baire space}. 
@@ -57,11 +68,11 @@
     Finally, suppose that $\bracsn{C(n_1, \cdots, n_N)| \bracsn{n_k}_1^N \subset \natp, N \in \natp} \subset 2^X$ has been constructed to satisfy (i)-(iv). Since $X$ is complete, for each $\seq{n_k} \in \mathscr{N}$, there exists a unique $f(\seq{n_k}) \in X$ such that $\bracs{f(\seq{n_k})} = \bigcap_{N \in \natp}C(n_1, \cdots, n_N)$. For each $x \in X$, (iii) and (iv) imply that there exists $\seq{n_k} \in \mathscr{N}$ such that $x = f(\seq{n_k})$. As such, $f: \mathscr{N} \to X$ is a surjective mapping. For any $\seq{m_k}, \seq{n_k} \in \mathscr{N}$ and $N \in \natp$ with $m_k = n_k$ for each $1 \le k \le N$, $d(f(\seq{m_k}), f(\seq{n_k})) \le 1/N$. Therefore $f \in C(\mathscr{N}; X)$. 
 \end{proof}
 
-\begin{proposition}
-\label{proposition:cantor-universality}
+\begin{theorem}[Alexandroff-Hausdorff]
+\label{theorem:cantor-universality}
     Let $X$ be a non-empty compact metrisable space, then there exists a surjective mapping $f \in C(2^{\natp}; X)$. 
-\end{proposition}
-\begin{proof}
+\end{theorem}
+\begin{proof}[Proof, adapted from {{\cite[Proposition 8.2.7]{CohnMeasure}}}. ]
     Let $d: X \times X \to [0, \infty)$ be a metric on $X$. Since $X$ is compact, for each $N \in \natp$, there exists $K_N \in \natp$ and $\seqf{x_{N, k}|1 \le k \le K_N} \subset X$ such that $X = \bigcup_{k = 1}^{K_N}B(x_{N, k}, 1/N)$.
 
     To construct the desired map, it is sufficient to construct