From 4e451700d22e7096136b6b16f4b914497bf353cb Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Sun, 25 Jan 2026 12:29:04 -0500
Subject: [PATCH] Added the metrisability of TVS.

---
 src/fa/tvs/metric.tex | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/fa/tvs/metric.tex b/src/fa/tvs/metric.tex
index 8d1416d..2bdf8c0 100644
--- a/src/fa/tvs/metric.tex
+++ b/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}