Added metrisability of locally bounded spaces.

src/fa/tvs/metric.tex

@@ -137,3 +137,16 @@
 
     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}
+
+\begin{definition}[Locally Bounded]
+\label{definition:locally-bounded}
+    Let $E$ be a TVS over $K \in \RC$, then $E$ is \textbf{locally bounded} if there exists $U \in \cn^o(0)$ bounded.
+\end{definition}
+
+\begin{proposition}[{{\cite[1.6.2]{SchaeferWolff}}}]
+\label{proposition:locally-bounded-metrisable}
+    Let $E$ be a locally bounded TVS over $K \in \RC$, then there exists a pseudonorm $\rho: E \to [0, \infty)$ that induces the topology on $E$.
+\end{proposition}
+\begin{proof}
+    Let $U \in \cn^o(0)$ be bounded. Using \ref{proposition:tvs-good-neighbourhood-base}, assume without loss of generality that $U$ is circled. For each $n \in \natp$, let $U_n = n^{-1}U$. Let $V \in \cn^o(0)$, then there exists $\lambda \in K$ such that $\lambda V \supset U$, $\abs{\lambda}^{-1}U \subset V$. For any $n \in \natp$ with $n^{-1} < \abs{\lambda}^{-1}$, $U_n \subset V$. Thus $E$ admits a countable fundamental system of neighbourhoods at $0$. By \ref{theorem:tvs-metrisable}, the topology on $E$ is induced by a pseudonorm.
+\end{proof}