Symmetry of the derivative (normed/frechet).

src/fa/lc/index.tex

@@ -8,3 +8,4 @@
 \input{./src/fa/lc/projective.tex}
 \input{./src/fa/lc/inductive.tex}
 \input{./src/fa/lc/hahn-banach.tex}
+\input{./src/fa/lc/spaces-of-linear.tex}

src/fa/lc/spaces-of-linear.tex

@@ -0,0 +1,18 @@
+\section{Locally Convex Spaces of Linear Maps}
+\label{section:lc-spaces-linear-map}
+
+\begin{proposition}
+\label{proposition:lc-spaces-linear-map}
+    Let $T$ be a set, $E$ be a locally convex space defined by the seminorms $\seqi{[\cdot]}$, and $\mathfrak{S} \subset 2^T$ be an upward-directed family. For each $i \in I$ and $S \in \mathfrak{S}$, let
+    \[
+    [\cdot]_{S, i}: E^T \to [0, \infty) \quad f \mapsto \sup_{x \in S}[f(x)]_{S, i}
+    \]
+    then the $\mathfrak{S}$-uniform topology on $E^T$ is defined by the seminorms
+    \[
+    \bracs{[\cdot]_{S, i}|S \in \mathfrak{S}, i \in I}
+    \]
+    and hence locally convex.
+\end{proposition}
+\begin{proof}
+    By \ref{proposition:set-uniform-pseudometric}.
+\end{proof}