Added the metrisability of TVS.

src/fa/tvs/metric.tex

@@ -114,3 +114,26 @@
 
 	As discussed in \ref{remark:uniform-sequence-pseudometric} on the proof of \ref{lemma:uniform-sequence-pseudometric}, constructing a pseudometric from entourages by building its level sets is difficult because composing symmetric entourages does not necessarily lead to symmetric entourages. The topological vector space does not have this shortcoming, and as such allows this construction.
 \end{remark}
+
+\begin{theorem}[Metrisability of Topological Vector Spaces]
+\label{theorem:tvs-metrisable}
+    Let $E$ be a TVS over $K \in \RC$, then the following are equivalent:
+    \begin{enumerate}
+        \item There exists a pseudonorm that induces the topology on $E$.
+        \item There exists a translation-invariant pseudometric that induces the topology on $E$.
+        \item $E$ admits a countable fundamental system of entourages.
+        \item There exists a pseudometric that induces the topology on $E$.
+        \item $E$ admits a countable fundamental system of neighbourhoods at $0$.
+    \end{enumerate}
+\end{theorem}
+\begin{proof}
+    (3) $\Rightarrow$ (4): By \ref{theorem:uniform-metrisable}.
+
+    (4) $\Rightarrow$ (1): By \ref{proposition:tvs-good-neighbourhood-base}, there exists $\seq{U_n} \subset \cn_E(0)$ circled and radial such that for each $n \in \natp$, $U_{n+1} + U_{n+1} \subset U_n$. By \ref{lemma:tvs-sequence-pseudonorm}, there exists a pseudonorm $\rho: E \to [0, \infty)$ such that for each $N \in \natp$, $U_{n+1} \subset \rho^{-1}([0, 2^{-n})) \subset U_{n}$. In which case, $\rho$ induces the topology on $E$.
+\end{proof}
+
+\begin{remark}
+    \label{remark:tvs-metrisable}
+
+    Let $E$ be a TVS over $K \in \RC$. Similar to the case of uniform spaces, there exists a family of pseudonorms $\seqi{\rho}$ that induces the topology on $E$. Using Minkowski functionals (\ref{definition:gauge}), $\seqi{\rho}$ can be taken such that $\rho_i(\lambda x) = \abs{\lambda}\rho_i(x)$ for all $x \in E$ and $\lambda \in K$. However, a single pseudonorm with this property cannot always induce the topology even if the space is metrisable, hence the difference between pseudonorms and seminorms.
+\end{remark}