Added neighbourhood characterisation for TVS.

src/fa/tvs/definition.tex

@@ -147,3 +147,46 @@
 
     Let $U \in \cn(0)$ be closed, then there exists a balanced neighbourhood $V \in \cn^o(0)$ such that $V \subset U$. In which case, for any $\lambda \in K$ with $0 < \abs{\lambda} \le 1$, $\lambda \overline{V} = \overline{\lambda V} \subset \overline{V}$ by (TVS2). Therefore $\overline{V} \subset U$ is balanced as well.
 \end{proof}
+
+\begin{proposition}[{{\cite[1.2]{SchaeferWolff}}}]
+\label{proposition:tvs-0-neighbourhood-base}
+    Let $E$ be a vector space of $K \in \RC$, and $\topo$ be a vector space topology on $E$, then there exists a fundamental system of neighbourhoods $\fB \subset \cn_E(0)$ such that:
+    \begin{enumerate}
+        \item[(TVB1)] For each $U \in \fB$, there exists $V \in \fB$ such that $V + V \subset U$.
+        \item[(TVB2)] For each $U \in \fB$, $U$ is circled and radial.
+    \end{enumerate}
+    Conversely, if $\fB \subset 2^E$ is a family of sets that contain $0$ and satisfies (TVB1) and (TVB2), then there exists a unique topology $\topo$ on $E$ for which $\fB$ is a fundamental system of neighbourhoods at $0$.
+\end{proposition}
+\begin{proof}
+    (1): By \ref{proposition:tvs-good-neighbourhood-base}, there exists a fundamental system of neighbourhoods $\fB \subset \cn_E(0)$ consisting of circled and radial sets. By (TVS1), $\fB$ satisfies (TVB1).
+
+    (2): For each $V \in \fB$, let $U_V = \bracs{(x, y) \in E|x - y \in V}$, then $U_V$ is symmetric and translation-invariant by (TVB1). Let
+    \[
+    \mathfrak{V} = \bracs{U_V|V \in \fB}
+    \]
+    then
+    \begin{enumerate}
+        \item[(FB1)] For any $V, V' \in \fB$, there exists $W \in \fB$ with $W \subset V \cap V'$. In which case, $U_{V} \cap U_{V'} \supset U_W \in \mathfrak{V}$.
+        \item[(UB1)] For any $x \in E$ and $V \in \fB$, $x - x = 0 \in V$, so $\Delta \subset U_V$.
+        \item[(UB2)] For any $V \in \fB$, by (TVB1), there exists $W \in \fB$ such that $W + W \subset V$. In which case, for any $x, y, z \in E$ with $x - y, y - z \in W$, $x - z \in V$. Therefore $U_W \circ U_W \subset U_V$.
+    \end{enumerate}
+    By \ref{proposition:fundamental-entourage-criterion}, there exists a unique uniformity $\fU$ on $E$ for which $\mathfrak{V}$ is a fundamental system of entourages.
+
+    It remains to verify that $\mathfrak{V}$ induces a vector space topology on $E$.
+    \begin{enumerate}
+        \item[(TVS1)] Let $V \in \fB$, then there exists $W \in \fB$ such that $W + W \subset V$ by (TVB1). In which case, for any $x, x', y, y'$ with $x - x' \in W$ and $y - y' \in W$, $(x + y) - (x' + y') \in W + W \subset V$.
+        \item[(TVS2)] Let $V \in \fB$, $\eps > 0$, $x, x' \in E$ with $x - x' \in V$, and $\lambda, \lambda' \in K$ with $\abs{\lambda - \lambda'} < \eps$, then
+        \begin{align*}
+            \lambda x - \lambda' x' &= \lambda x - \lambda x' + \lambda x' - \lambda' x' \\
+            &= \lambda(x - x') + (\lambda - \lambda')x' \in \lambda V + (\lambda - \lambda')x'
+        \end{align*}
+        Since $V$ is radial, there exists $\mu \in K$ such that $x \in \mu V$. Given that $V$ is circled, $x' = x + (x - x') \in \mu V + V \subset (\abs{\mu} + 1)V$, and
+        \[
+        \lambda x - \lambda' x' \in \lambda V + \eps(\abs \mu + 1)V \subset \abs{\lambda} V + \eps(\abs \mu + 1)V
+        \]
+
+        Let $W \in \fB$ and $\eps > 0$ such that $\eps(\abs{\mu}+1) \le 1$, then by repeated application of (TVB1), there exists $V \in \fB$ such that $\abs{\lambda} V + V \subset W$. Therefore scalar multiplication is jointly continuous.
+    \end{enumerate}
+
+    Finally, by definition of the uniform topology, $\fB = \bracs{U_V(0)|V \in \fB}$ is a fundamental system of neighbourhoods at $0$.
+\end{proof}