Upgraded the separable dual lemma.

src/fa/norm/separable.tex

@@ -3,14 +3,16 @@
 
 \begin{proposition}
 \label{proposition:separable-dual}
-    Let $K \in \RC$ and $\dpn{E, F}{\lambda}$ be a duality of normed vector spaces over $K$ with $E$ being separable, then
+    Let $K \in \RC$ and $\dpn{E, F}{\lambda}$ be a duality of normed vector spaces over $K$ with $E$ being separable, and $S = \bracsn{y \in F|\ \norm{y}_F \le 1}$ be the closed unit ball of $F$, then
     \begin{enumerate}
-        \item The closed unit ball $S = \bracsn{y \in F|\ \norm{y}_{F} \le 1}$ is separable with respect to the $\sigma(F, E)$-topology. 
+        \item $S$ is separable with respect to the $\sigma(F, E)$-topology. 
+        \item $S$ is metrisable with respect to the $\sigma(F, E)$-topology. 
+        \item For any $A \subset F$, $A$ is separable with respect to the $\sigma(F, E)$-topology. 
         \item If the duality is norming, then there exists $\seq{y_n} \subset F$ such that for each $x \in E$, $\norm{x}_E = \sup_{n \in \natp}|\dpn{x, y_n}{\lambda}|$. 
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    Let $\seq{x_n} \subset E$ be a dense subset. For each $N \in \natp$, let
+    (1): Let $\seq{x_n} \subset E$ be a dense subset. For each $N \in \natp$, let
     \[
     T_N: S \to \real^N \quad y \mapsto (\dpn{x_1, y}{E}, \cdots, \dpn{x_N, y}{E})
     \]
@@ -23,6 +25,10 @@
     \] 
 
     Thus for each $N \in \natp$, $\dpn{x_n, y_{N, k_N}}{E} \to \dpn{x_n, y}{E}$ as $N \to \infty$. Since $\phi_{N, k_N} \to \phi$ pointwise on a dense subset of $E$, and $\bracsn{y_{N, k_N}|N \in \natp} \subset S$ is uniformly equicontinuous, $\phi_{N, k_N} \to \phi$ in the $\sigma(F, E)$-topology by \autoref{proposition:strong-operator-dense}. 
+
+    (2): Let $\seq{x_n} \subset E$ be a dense subset, then by \autoref{proposition:strong-operator-dense}, the $\sigma(F, E)$-topology on $S$ is induced by $\seq{x_n}$, and hence metrisable by \autoref{theorem:uniform-metrisable}. 
+
+    (3): For any $A \subset E$, $A = \bigcup_{n \in \natp}A \cap nS$. By \autoref{proposition:separable-metric-space}, $A \cap nS$ is separable for each $n \in \natp$. Therefore $A$ is also separable. 
 \end{proof}
 
 \begin{proposition}