Added more bits on bornologic spaces.

src/fa/lc/barrel.tex

@@ -23,7 +23,7 @@
     $(3) \Rightarrow (2)$: Let $D \subset E$ be a barrel and $\rho: E \to [0, \infty)$ be its gauge. By (4) of \autoref{definition:gauge}, $D = \bracs{\rho \le 1}$, so $\bracs{\rho > 1}$ is open, and $\rho$ is semicontinuous. By assumption, $\rho$ is continuous, so $D \in \cn_E(0)$ by (5) of \autoref{lemma:continuous-seminorm}. 
 \end{proof}
 
-\begin{summary}[Barreled Spaces]
+\begin{summary}
 \label{summary:barreled-space}
     The following types of locally convex spaces are barreled:
     \begin{enumerate}
@@ -61,7 +61,7 @@
 \label{proposition:barrel-limit}
     Let $\seqi{E}$ be locally convex 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 the inductive locally convex topology on $E$ induced by $\seqi{T}$ is barreled.  
 \end{proposition}
-\begin{proof}[Proof, {{\cite[II.7.2]{SchaeferWolff}}}]
+\begin{proof}[Proof, {{\cite[II.7.2]{SchaeferWolff}}}. ]
     Let $D \subset E$ be a barrel, then for each $i \in I$, $T_i^{-1}(D) \subset E_i$ is also a barrel, and thus a neighbourhood of $0$ in $E_i$. By (5) of \autoref{definition:lc-inductive}, $D$ is a neighbourhood of $0$ in $E$, so $E$ is barreled. 
 \end{proof}
 

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.

src/fa/rs/bv.tex

@@ -65,7 +65,7 @@
     \begin{enumerate}
         \item $BV([a, b]; E)$ is a vector space.
         \item For each continuous seminorm $\rho$ on $E$, $[\cdot]_{\text{var}, \rho}$ is a seminorm on $BV([a, b]; E)$.
-        \item For each continuous seminorm $\rho$ on $E$ and $M > 0$, $\bracs{[\cdot]_{\text{var}, \rho} \le M} \subset E^{[a, b]}$ is closed. 
+        \item For each continuous seminorm $\rho$ on $E$, $[\cdot]_{\text{var}, \rho}: E^{[a, b]} \to [0, \infty]$ is lower semicontinuous. In particular, for any $M > 0$, $\bracs{[\cdot]_{\text{var}, \rho} \le M} \subset E^{[a, b]}$ is closed. 
         \item For any $f \in BV([a, b]; E)$ and continuous seminorm $\rho$ on $E$, $\sup_{x \in [a, b]}\rho(f(x)) \le \rho(f(a)) + [f]_{\text{var}, \rho}$.
     \end{enumerate}
     If $(E, \norm{\cdot}_E)$ is a normed vector space, then
@@ -74,15 +74,7 @@
     \end{enumerate}
 \end{definition}
 \begin{proof}[Proof {{\cite[Proposition X.1.1]{Lang}}}. ]
-    (3): Let $\rho$ be a continuous seminorm on $E$, $P = \seqf{x_j} \in \scp([a, b])$, and $f \in \overline{\bracs{[\cdot]_{\text{var}, \rho} \le M}}$. For any $\eps > 0$, there exists $g \in \bracs{[\cdot]_{\text{var}, \rho} \le M}$ such that $\rho(f(x_j) - g(x_j)) < \eps$ for each $1 \le j \le n$. In which case, 
-    \begin{align*}
-    V_{\rho, P}(f) &= \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1})) \\
-    &\le 2n\eps + \sum_{j = 1}^n \rho(g(x_j) - g(x_{j - 1})) \\
-    &\le V_{\rho, P}(g) + 2n\eps \le M + 2n\eps
-    \end{align*}
-    
-
-    As the above holds for all $\eps > 0$, $V_{\rho, P}(f) \le M$. Since this holds for all $P \in \scp([a, b])$, $[f]_{\text{var}, \rho} \le M$.
+    (3): For each $P \in \scp([a, b])$, the mapping $V_{P, \rho}: E^{[a, b]} \to [0, \infty]$ is continuous. Since $[\cdot]_{\text{var}, \rho} = \sup_{P \in \scp([a, b])}V_{P, \rho}$, $[\cdot]_{\text{var}, \rho}$ is lower semicontinuous by \autoref{proposition:semicontinuous-properties}. 
 
     (5): For each $n \in \nat^+$, let
     \[

src/fa/tvs/bounded.tex

@@ -3,8 +3,19 @@
 
 \begin{definition}[Bounded]
 \label{definition:bounded}
-    Let $E$ be a TVS over $K \in \RC$ and $B \subset E$, then $B$ is \textbf{bounded} if for every $U \in \cn(0)$, there exists $\lambda \in K$ such that $\lambda U \supset B$. The collection $B(E)$ is the set of all bounded sets of $E$.
+    Let $E$ be a TVS over $K \in \RC$ and $B \subset E$, then the following are equivalent:
+    \begin{enumerate}
+        \item For every $U \in \cn(0)$, there exists $\lambda \in K$ such that $\lambda U \supset B$. 
+        \item For every $\seq{x_n} \subset B$ and $\seq{\lambda_n} \subset K$ such that $\lambda_n \to 0$, $\lambda_n x_n \to 0$ as $n \to \infty$.
+    \end{enumerate}
+
+    If the above holds, then $B$ is \textbf{bounded}. The collection $B(E)$ is the set of all bounded sets of $E$.
 \end{definition}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let $U \in \cn_E(0)$ be circled, then there exists $k \in \natp$ such that $kU \supset B$. Since $\lambda_n \to 0$ as $n \to \infty$, there exists $N \in \natp$ such that $|\lambda_n| \le 1/k$ for all $n \ge N$. In which case, $\lambda_n x_n \in \lambda_n B \subset U$ for all $n \ge N$. 
+
+    $\neg (1) \Rightarrow \neg (2)$: Let $U \in \cn_E(0)$ be circled such that $B \not\subset nU$ for all $n \in \natp$. For each $n \in \natp$, let $x_n \in B \setminus nU$, then $x_n/n \not\in U$ for all $n \in \natp$. 
+\end{proof}
 
 \begin{proposition}[{{\cite[I.5.1]{SchaeferWolff}}}]
 \label{proposition:bounded-operations}