Me when I forget to commit.

src/topology/main/interiorclosureboundary.tex

@@ -78,6 +78,15 @@
     Let $x \in \prod_{i \in I}X_i$ and $U \in \cn(x)$, then there exists $J \subset I$ finite and $\seqf{U_j}$ such that $U_j \in \cn(\pi_j(x))$ for each $j \in J$, and $x \in \bigcap_{j \in J}\pi_j^{-1}(U_j) \subset U$. By density of each $A_j$, there exists $y \in X$ such that $y_j \in U_j$ for each $j \in J$. Thus $y \in U$, and $A$ is dense.
 \end{proof}
 
+\begin{proposition}
+\label{proposition:separable-product}
+    Let $\seqf{X_j}$ be separable topological spaces, then $\prod_{j = 1}^n X_j$ is also separable.
+\end{proposition}
+\begin{proof}
+    Let $\seq{A_j}$ such that $A_j \subset X_j$ is countable and dense for each $1 \le j \le n$. By \ref{proposition:dense-product}, $\prod_{j = 1}^n A_j$ is countable and dense in $\prod_{j = 1}^n X_j$.
+\end{proof}
+
+
 \begin{lemma}
 \label{lemma:closurecomplement}
     Let $X$ be a topological space and $A \subset X$, then $(A^o)^c = \overline{A^c}$.

src/topology/main/metric.tex

@@ -1,50 +0,0 @@
-\section{Metric Spaces}
-\label{section:metric}
-
-\begin{definition}[Metric]
-\label{definition:metric}
-    Let $X$ be a set, a \textbf{pseudo-metric} is a mapping $d: X \times X \to [0, \infty)$ such that:
-    \begin{enumerate}
-        \item For any $x \in X$, $d(x, x) = 0$.
-        \item For any $x, y \in X$, $d(x, y) = d(y, x)$.
-        \item For any $x, y, z \in X$, $d(x, z) \le d(x, y) + d(y, z)$.
-    \end{enumerate}
-    and the pair $(X, d)$ is a \textbf{pseudo-metric space}. If in addition,
-    \begin{enumerate}
-        \item[(4)] For any $x, y \in X$, $d(x, y) = 0$ if and only if $x = y$.
-    \end{enumerate}
-    then $d$ is a \textbf{metric}.
-\end{definition}
-
-\begin{definition}[Induced Uniformity]
-\label{definition:metric-uniformity}
-    Let $(X, d)$ be a metric space. For each $r > 0$, let
-    \[
-    U_r = \bracs{(x, y) \in X \times Y| d(x, y) < r}
-    \]
-    then there exists a uniformity $\fU$ on $X$ such that the family $\fB = \bracs{U_r| r > 0}$ is a fundamental system of entourages for $\fU$, known as the \textbf{uniformity induced by} $d$.
-
-    Let $\seqi{d}$ be pseudo-metrics on $X$. For each $i \in I$, let $X_i = X$ be equipped with the uniformity induced by $d_i$, then the \textbf{uniformity induced by} $\seqi{d}$ is the initial uniformity generated by the identity $\text{Id}_X: X \to X_i$.
-\end{definition}
-
-\begin{lemma}
-\label{lemma:uniform-first-countable}
-    Let $X$ be a uniform space with a countable fundamental system of entourages, then there exists a countable fundamental system of symmetric entourages $\fB = \bracs{U_{1/2^n}|n \in \nat^+}$ such that $U_{1/2^{n+1}} \circ U_{1/2^{n+1}} \subset U_{1/2^n}$ for all $n \in \nat^+$.
-\end{lemma}
-\begin{proof}
-    Let $\seq{V}$ be a countable fundamental system of entourages. By \ref{lemma:symmetricfundamentalentourage}, there exists a symmetric entourage $U_{1/2} \subset V_1$. Suppose inductively that $U_{1/2^n}$ has been constructed, then by (U2) and \ref{lemma:symmetricfundamentalentourage}, there exists a symmetric entourage $U_{1/2^{n+1}} \subset U_{1/2^n} \cap V$. Thus $\fB = \bracs{U_{1/2^n}|n \in \nat^+}$ is the desired family.
-\end{proof}
-
-% Work in progress: pseudo-metrisability of uniform spaces.
-
-\begin{lemma}
-\label{lemma:uniform-urysohn}
-    Let $X$ be a uniform space with a countable fundamental system of entourages, $\mathbb{D}$ be the dyadic rational numbers in $[0, 1]$, then there exists a fundamental system of entourages $\fB = \bracs{}$
-\end{lemma}
-
-
-
-\begin{proposition}
-\label{proposition:uniform-pseudometric}
-    Let
-\end{proposition}

src/topology/main/neighbourhoods.tex

@@ -22,7 +22,6 @@
 \label{lemma:openneighbourhood}
     Let $(X, \topo)$ be a topological space, then $U \subset X$ is open if and only if $U \in \cn_\topo(x)$ for all $x \in U$.
 \end{lemma}
-
 \begin{proof}
     Suppose that $U \in \cn_\topo(x)$ for all $x \in U$. For each $x \in U$, there exists $V_x \in \topo$ with $x \in V_x \subset U$.
     Thus $U = \bigcup_{x \in U}V_x \in \topo$.

src/topology/main/normal.tex

@@ -82,6 +82,6 @@
 
     Since $\real$ is complete, so is $BC(X; \real)$ by \ref{proposition:set-uniform-complete}. Using successive approximations (\ref{theorem:successive-approximation}), for every $f \in BC(A; \real)$, there exists $F \in BC(X; \real)$ such that $RF = F|_A = f$ and
     \[
-    \norm{F}_u \le \frac{1}{3} \cdot \frac{1}{1 - 2/3} \cdot \norm{f}_u = 1
+    \norm{F}_u \le \frac{1}{3} \cdot \frac{1}{1 - 2/3} \cdot \norm{f}_u = \norm{f}_u
     \]
 \end{proof}