Housekeeping.

src/topology/metric/metric.tex

@@ -36,8 +36,6 @@
 
     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$.