From 7e78ce4ae1ff3cc8e2499e66d933db062bc32a17 Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Tue, 11 Aug 2026 13:50:38 -0400
Subject: [PATCH] Simplified the separable dual result.

---
 src/fa/norm/separable.tex | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/src/fa/norm/separable.tex b/src/fa/norm/separable.tex
index fe3cde1..373b1bc 100644
--- a/src/fa/norm/separable.tex
+++ b/src/fa/norm/separable.tex
@@ -12,22 +12,8 @@
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    (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}{\lambda}, \cdots, \dpn{x_N, y}{\lambda})
-    \]
-
-    Since $\real^N$ is separable, $T_N(S)$ is separable by \autoref{proposition:separable-metric-space}. Thus there exists $\bracs{y_{N, k}}_{k = 1}^\infty \subset S$ such that $\bracs{T_Ny_{N, k}}_{k = 1}^\infty$ is dense in $T_N(S)$.
-
-    Let $y \in S$, then for each $N \in \natp$, there exists $k_N \in \natp$ such that for each $1 \le n \le N$, 
-    \[
-    |\dpn{x_n, y_{N, k_N}}{\lambda} - \dpn{x_n, y}{\lambda}| \le \frac{1}{N}
-    \] 
-
-    Thus for each $N \in \natp$, $\dpn{x_n, y_{N, k_N}}{\lambda} \to \dpn{x_n, y}{\lambda}$ as $N \to \infty$. Since $y_{N, k_N} \to y$ pointwise on a dense subset of $E$ and $\bracsn{y_{N, k_N}|N \in \natp} \subset S$ is uniformly equicontinuous, $y_{N, k_N} \to y$ 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}. 
-
+    (1), (2): Let $D \subset E$ be a countable dense subset. By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}, $S$ is embedded as a subspace of $\real^D$. By \autoref{theorem:uniform-metrisable}, $\real^D$ is metrisable. By \autoref{proposition:separable-product}, $\real^D$ is separable. Thus $S$ is also metrisable and separable by \autoref{proposition:separable-metric-space}. 
+    
     (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}