More housekeeping

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}

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}