Various additions.

src/fa/norm/separable.tex

@@ -56,4 +56,31 @@
     then $\phi_x$ is Borel measurable with respect to the weak topology, so $B(x, r) = \bracs{\phi_x < r}$ is a Borel set with respect to the weak topology. 
 \end{proof}
 
+\begin{lemma}
+\label{lemma:compact-embed}
+    Let $E$ be a normed vector space over $K \in \RC$ and $A \subset [0, 1]$ be closed, then $C(A; E)$ embeds isometrically into $C([0, 1]; E)$. 
+\end{lemma}
+\begin{proof}
+    First note that if $0 \not\in A$ or $1 \not\in A$, $C(A; E)$ embeds isometrically into $C(A \cup \bracs{0, 1}; E)$ through extension by $0$. Thus assume without loss of generality that $A$ contains the endpoints $0$ and $1$. 
+
+    Let $U = [0, 1] \setminus A$, then there exists $\seq{(a_n, b_n)} \subset [0, 1]^2$ such that  $U = \bigsqcup_{n \in \natp}(a_n, b_n)$. For each $f \in C(A; E)$, let
+    \[
+    Tf: [0, 1] \to E \quad x \mapsto \begin{cases}
+        f(x) &x \in A \\
+         \frac{b_n - x}{b_n - a_n}f(a_n) + \frac{x - a_n}{b_n - a_n}f(b_n) &x \in (a_n, b_n) \subset [0, 1]
+    \end{cases}
+    \]
+
+    then the mapping $f \mapsto Tf$ is an isometric embedding into $E^{[0, 1]}$ with respect to the uniform norm.
+    
+    Since $U$ is open and $Tf$ is affine on each component of $U$, $Tf$ is continuous on $U$. It remains to show that $Tf$ is continuous on $A$. Let $x \in A$ and $\eps > 0$, then there exists $\delta > 0$ such that $\norm{f(y) - f(x)}_E < \eps$ for all $y \in (x -\delta, x + \delta) \cap A$. Now, a case analysis: 
+    \begin{enumerate}
+        \item If there exists $y \in (x - \delta, x) \cap A$, then for any $z \in U \cap (y, x)$, there exists $n \in \natp$ such that $(a_n, b_n) \subset (y, x)$ and $z \in (a_n, b_n)$. In which case, since $\norm{f(a_n) - f(x)}_E < \eps$ and $\norm{f(b_n) - f(x)}_E < \eps$, $\norm{Tf(z) - Tf(x)}_E < \eps$. Thus $\norm{Tf(z) - Tf(x)}_E < \eps$ for all $z \in (y, x)$.
+        \item Otherwise, $x = 0$ or $Tf|_{(x - \delta, x)}$ is an affine function. Either way, there exists $y \in (x - \delta, x)$ such that $\norm{Tf(z) - Tf(x)}_E < \eps$ for all $z \in (y, x) \cap [0, 1]$. 
+    \end{enumerate}
+
+    Thus there exists $y \in (x - \delta, x)$ with $\norm{Tf(z) - Tf(x)}_E < \eps$ for all $z \in (y, x) \cap [0, 1]$. Similarly, there exists $y' \in (x, x + \delta)$ with $\norm{Tf(z) - Tf(x)}_E < \eps$ for all $z \in (x, y') \cap [0, 1]$. Therefore $Tf$ is continuous at $x$. Since this holds for all $x \in U$ and $x \in A$, $Tf \in C([0, 1]; E)$. 
+\end{proof}
+
+