From 714925d34b31f206079d56ac808848051eb694bd Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Thu, 29 Oct 2026 16:24:08 -0400
Subject: [PATCH] More housekeeping

---
 src/fa/norm/separable.tex      |  6 +++---
 src/fa/tvs/complete-metric.tex | 29 ++++++++++++++++++++++++++++-
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/src/fa/norm/separable.tex b/src/fa/norm/separable.tex
index c3dcd64..a781770 100644
--- a/src/fa/norm/separable.tex
+++ b/src/fa/norm/separable.tex
@@ -12,7 +12,7 @@
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    (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 $K^D$. By \autoref{theorem:uniform-metrisable}, $\real^D$ is metrisable. By \autoref{proposition:separable-product}, $K^D$ is separable. Thus $S$ is also metrisable and separable by \autoref{proposition:separable-metric-space}. 
+    (1), (2): Let $D \subset E$ be a countable dense subset. By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}, the topology of pointwise convergence on $E$ and the topology of pointwise convergence on $E$ coincide on $S$, so $S$ is embedded as a subspace of $K^D$. By \autoref{theorem:uniform-metrisable}, $K^D$ is metrisable. By \autoref{proposition:separable-product}, $K^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}
@@ -63,8 +63,8 @@
     Finally, \autoref{lemma:compact-embed} provides yet another linear isometric embedding $C(\mathcal{C}; K) \to C([0, 1]; K)$. Composing the above maps as follows
     \[
     \xymatrix{
-E \ar@{->}[r] & C(B; K) \ar@{->}[r] & C(2^{{\mathbb N}^+}; K) \ar@{->}[r] & C(\mathcal{C}; K) \ar@{->}[r] & C([0, 1]; K)
-}
+    E \ar@{->}[r] & C(B; K) \ar@{->}[r] & C(2^{{\mathbb N}^+}; K) \ar@{->}[r] & C(\mathcal{C}; K) \ar@{->}[r] & C([0, 1]; K)
+    }
     \]
 
     yields the desired embedding. 
diff --git a/src/fa/tvs/complete-metric.tex b/src/fa/tvs/complete-metric.tex
index 8eefa3f..93534d7 100644
--- a/src/fa/tvs/complete-metric.tex
+++ b/src/fa/tvs/complete-metric.tex
@@ -150,7 +150,6 @@
 
 \end{proof}
 
-
 \begin{example}
     \label{example:open-mapping-counters}
 
@@ -160,3 +159,31 @@
 \end{example}
 
 
+\begin{theorem}[Closed Complementation Theorem]
+\label{theorem:closed-complement}
+    Let $E$ be a complete metric TVS, $\bracsn{0} \ne F \subsetneq E$ be a closed subspace, then the following are equivalent:
+    \begin{enumerate}
+        \item $F$ admits a closed complementary subspace. 
+        \item There exists $P \in L(E; E)$ such that $P^2 = P$ and $P(E) = F$.
+    \end{enumerate}
+\end{theorem}
+\begin{proof}
+    (2) $\Rightarrow$ (1): Let $G = \ker(P)$, then the mapping
+    \[
+    E \to F \times G \quad x \mapsto (Px, (1 - P)x)
+    \]
+
+    is a toplinaer isomorphism. 
+
+    (1) $\Rightarrow$ (2): Let $G$ be a closed complementary subspace of $E$, so that the mapping
+    \[
+    T: F \times G \to E \quad (x, y) \mapsto x + y
+    \]
+
+    is a continuous, bijective linear map. As $F, G \subset E$ are both closed, they are complete by \autoref{proposition:complete-closed}, and $E \times F$ is a complete metric TVS by \autoref{proposition:product-complete}. By the \hyperref[Open Mapping Theorem]{theorem:open-mapping}, the $T$ is a toplinear isomorphism. As such, $P$ is given by the following composition
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{T^{-1}} & F \times G \ar@{->}[r]^{\pi_1} & F
+    }
+    \]
+\end{proof}