Added more bits on bornologic spaces.

src/fa/lc/bornologic.tex

@@ -22,6 +22,21 @@
     (2) $\Rightarrow$ (1): Let $\rho$ be the \hyperref[gauge]{definition:gauge} of $U$, then for any $B \subset E$ bounded, there exists $R > 0$ such that $B \subset RU$. In which case, $\rho(B) \subset [0, R]$. 
 \end{proof}
 
+\begin{proposition}
+\label{proposition:bornologic-bounded}
+    Let $E$ be a bornologic space, $F$ be a locally convex space, and $T \in \hom(E; F)$, then the following are equivalent:
+    \begin{enumerate}
+        \item $T$ is continuous.
+        \item $T$ is sequentially continuous. 
+        \item $T$ is bounded.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (2) $\Rightarrow$ (3): Let $B \subset E$ be a bounded set, $\seq{x_n} \subset E$, and $\seq{\lambda_n} \subset K$ such that $\lambda_n \to 0$ as $n \to \infty$, then $\lambda_n x_n \to 0$ as $n \to \infty$. By sequential continuity of $T$, $T(\lambda_n x_n) \to 0$ as $n \to \infty$ as well. Thus $T(B)$ is also bounded. 
+
+    (3) $\Rightarrow$ (1): Let $\rho: F \to [0, \infty)$ be a continuous seminorm, then $\rho \circ T$ is a seminorm on $E$ that is bounded on bounded sets. Since $E$ is bornologic, $\rho \circ T$ is continuous. Therefore $T$ is continuous by \autoref{proposition:tvs-convex-morphism}.
+\end{proof}
+
 \begin{proposition}
 \label{proposition:metrisable-bornologic}
     Let $E$ be a metrisable locally convex space, then $E$ is bornologic.
@@ -31,20 +46,14 @@
 \end{proof}
 
 \begin{proposition}
-\label{proposition:bornologic-bounded}
-    Let $E$ be a bornologic space, $F$ be a locally convex space, and $T \in \hom(E; F)$, then the following are equivalent:
-    \begin{enumerate}
-        \item $T$ is continuous.
-        \item $T$ is bounded.
-    \end{enumerate}
-    
+\label{proposition:bornologic-limit}
+    Let $\seqi{E}$ be bornologic spaces over $K \in \RC$, $E$ be a vector space over $K$, and $\seqi{T}$ such that $T_i \in \hom(E_i; E)$ for all $i \in I$, then $E$ equipped with the inductive topology is bornolgic. 
 \end{proposition}
 \begin{proof}
-    (1) $\Rightarrow$ (2): By \autoref{proposition:continuous-bounded}. 
-
-    (2) $\Rightarrow$ (1): Let $\rho: F \to [0, \infty)$ be a continuous seminorm, then $\rho \circ T$ is a seminorm on $E$ that is bounded on bounded sets. Since $E$ is bornologic, $\rho \circ T$ is continuous. Therefore $T$ is continuous by \autoref{proposition:tvs-convex-morphism}.
+    Let $\rho: E \to [0, \infty)$ be a seminorm on $E$ that is bounded on all bounded sets. For each $i \in I$ and $B \subset E_i$ bounded, $T_i(B)$ is bounded by \autoref{proposition:bornologic-bounded}, and $\rho \circ T_i(B)$ is bounded by assumption. Thus for every $i \in I$, $\rho \circ T_i$ is continuous, so $\rho$ is continuous by (4) of \autoref{definition:lc-inductive}. 
 \end{proof}
 
+
 \begin{proposition}
 \label{proposition:bornologic-continuous-complete}
     Let $E$ be a bornologic space and $F$ be a complete separated locally convex space, then $L_b(E; F)$ is complete. In particular, $E^*$ equipped with the topology of bounded convergence is complete.