Added missing steps and fixed typos.

src/topology/metric/metric.tex

@@ -12,3 +12,33 @@
     \end{enumerate}
     The pair $(X, d)$ is a \textbf{metric space}, which comes with the metric uniformity induced by $d$, and the corresponding topology.
 \end{definition}
+
+\begin{proposition}
+\label{proposition:separable-metric-space}
+    Let $(X, d)$ be a metric space, then the following are equivalent:
+    \begin{enumerate}
+        \item $X$ is second countable. 
+        \item $X$ is Lindelöf.
+        \item $X$ is separable.
+    \end{enumerate}
+
+    In particular, since second countability is hereditary, separability and the Lindelöf property are both hereditary in metric spaces. 
+    
+\end{proposition}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let $\seqi{U} \subset 2^X$ be an open cover of $X$. Let $\seq{V_n} \subset 2^X$ be a countable base for the topology on $X$, and
+    \[
+    K = \bracs{n \in \natp| \exists i \in I: V_n \subset U_i}
+    \]
+
+    For any $x \in X$, there exists $i \in I$ such that $x \in U_i$, and $n \in \natp$ such that $x \in V_n \in U_i$. Therefore $\bigcup_{k \in K}V_k = X$. 
+
+    Let $J \subset I$ be countable such that for each $k \in K$, there exists $j \in J$ with $V_n \subset U_j$, then $X = \bigcup_{k \in K}V_k = \bigcup_{j \in J}V_j$.
+
+    % TODO: This stuff may be moved to more general spaces.
+
+    (2) $\Rightarrow$ (3): Let $n \in \nat$, then $\bracs{B(x, 1/n)|x \in X}$ is an open cover of $X$, so there exists $\seq{x_{n, k}} \subset X$ such that $X = \bigcup_{k \in \natp}B(x_k, 1/n)$. Let $D = \bracs{x_{n, k}| n, k \in \natp}$, then for any $x \in X$ and $n \in \natp$, there exists $k \in \natp$ such that $x \in B(x_{n, k}, 1/n)$, so $x_{n, k} \in B(x, 1/n)$. Therefore $D$ is dense in $X$, and $X$ is separable. 
+
+    (3) $\Rightarrow$ (1): Let $\seq{x_n} \subset X$ be a countable dense subset. Let $x \in X$ and $k \in \natp$, then there exists $x_n \in \natp$ such that $d(x, x_n) < 1/(2k)$. In which case, $x \in B(x_n, 1/(2k)) \subset B(x_n, 1/k)$. Therefore $\bracs{B(x_n, 1/k)|n, k \in \natp}$ forms a countable basis for $X$. 
+\end{proof}
+

src/topology/uniform/metric.tex

@@ -128,7 +128,7 @@ The axioms of uniform spaces strongly resembles working in a metric space. In fa
 
     and $d: X \times X \to [0, 1]$ by
     \[
-     d(x, y) = \inf\bracs{\sum_{j = 1}^n\rho(x_{j-1}, x_j) \bigg | \seqf{x_j} \subset X, x_0 = x, x_1 = y, n \in \natp}
+     d(x, y) = \inf\bracs{\sum_{j = 1}^n\rho(x_{j-1}, x_j) \bigg | \seqf{x_j} \subset X, x_0 = x, x_n = y, n \in \natp}
     \]
 
     then