Added bornological spaces.

src/fa/lc/convex.tex

@@ -199,3 +199,32 @@
 
     $(3) \Rightarrow (1)$: For each $i \in I$ and $r > 0$, $\bracs{x \in E| [x]_i < r}$ is convex.
 \end{proof}
+
+
+
+\begin{definition}[Associated Normed Space]
+\label{definition:lc-associated-normed-space}
+    Let $E$ be a separated locally convex space and $A \subset E$ be convex and circled. Let $E_0 = \bigcup_{n \in \natp}nA$, $\rho_0: E_0 \to [0, \infty)$ be the gauge of $A$, and $(E_A, \rho_A)$ be the quotient of $E_0$ by $\bracs{\phi = 0}$, equipped with the quotient norm of $\rho_0$, then
+    \begin{enumerate}
+        \item $(E_A, \rho_A)$ is a normed space. 
+    \end{enumerate}
+
+    If $A$ is radial, then $E_0 = E$ and the map $\pi_A: E \to E_A$ is the \textbf{canonical projection}, and
+    \begin{enumerate}[start=1]
+        \item If $A \in \cn_E(0)$, then $\pi_A \in L(E; E_A)$.
+    \end{enumerate}
+
+    If $(E_0, \rho_0)$ is separated, then $(E_0, \rho_0) = (E_A, \rho_A)$, and the map $\iota_A: E_A \to E$ is the \textbf{canonical inclusion}. In particular, if $A$ is bounded, then
+    \begin{enumerate}[start=2]
+        \item $(E_0, \rho_0)$ is separated. 
+        \item $\iota_A \in L(E_A; E)$. 
+    \end{enumerate}
+
+    The space $(E_A, \rho_A)$ is the \textbf{normed space associated with} $A$. 
+\end{definition}
+\begin{proof}
+    (3): Let $x \in E_0 \setminus \bracs{0}$. Since $E$ is separated, there exists $U \in \cn_E(0)$ such that $x \not\in U$. As $A$ is bounded, there exists $\lambda > 0$ such that $\lambda U \supset A$. In which case, $x \not\in \lambda^{-1}A$, and $E_0$ is separated. 
+
+    (4): Let $U \in \cn_E(0)$, then there exists $\lambda > 0$ such that $\lambda U \supset A$, so $\iota_A^{-1}(U) \supset \lambda^{-1}A \in \cn_{E_A}(0)$, and $\iota_A$ is continuous by \autoref{proposition:tvs-convex-morphism}.
+\end{proof}
+