Added monotone convergence for LSC functions.

src/fa/lc/hahn-banach.tex

@@ -132,17 +132,31 @@
     \begin{enumerate}
         \item For any subspace $M \subset E$, $x \in M \setminus E$, and continuous seminorm $\rho: E \to [0, \infty)$, there exists $\phi \in E^*$ such that
         \begin{enumerate}
-            \item $\phi \le \rho$.
+            \item $|\phi| \le \rho$.
             \item $\dpb{x, \phi}{E} = \inf_{y \in M}\rho(x + y)$.
         \end{enumerate}
-        \item For any $x \in E$ and continuous seminorm $\rho: E \to [0, \infty)$, there exists $\phi \in E^*$ with $\phi \le \rho$ and $\dpb{x, \phi}{E} = \rho(x)$.
+        \item For any $x \in E$ and continuous seminorm $\rho: E \to [0, \infty)$, there exists $\phi \in E^*$ with $|\phi| \le \rho$ and $\dpb{x, \phi}{E} = \rho(x)$.
         \item If $E$ is Hausdorff, then for any $x, y \in E$, there exists $\phi \in E^*$ with $\dpb{x, \phi}{E} \ne \dpb{y, \phi}{E}$.
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    (1): Let $\rho_M: E \to [0, \infty)$ be the quotient of $\rho$ by $M$, then $\rho_M \le \rho$ is a continuous seminorm on $E$ by \autoref{definition:quotient-norm}. Let $\phi_0: Kx \to K$ be defined by $\lambda x \mapsto \lambda \rho_M(x)$. By the \hyperref[Hahn-Banach theorem]{theorem:hahn-banach}, there exists $\phi \in \hom{E; K}$ such that $\dpb{x, \phi}{E} = \rho_M(x)$ and $\phi \le \rho_M \le \rho$.
+    (1): Let $\rho_M: E \to [0, \infty)$ be the quotient of $\rho$ by $M$, then $\rho_M \le \rho$ is a continuous seminorm on $E$ by \autoref{definition:quotient-norm}. Let $\phi_0: Kx \to K$ be defined by $\lambda x \mapsto \lambda \rho_M(x)$. By the \hyperref[Hahn-Banach theorem]{theorem:hahn-banach}, there exists $\phi \in \hom{E; K}$ such that $\dpb{x, \phi}{E} = \rho_M(x)$ and $|\phi| \le \rho_M \le \rho$.
 
     (2): By (1) applied to $M = \bracs{0}$.
 
     (3): By (2) applied to $x - y$.
 \end{proof}
+
+\begin{proposition}
+\label{proposition:seminorm-lsc}
+    Let $E$ be a locally convex space and $\rho: E \to [0, \infty)$ be a continuous seminorm, then $\rho: E_w \to [0, \infty)$ is lower semicontinuous and Borel measurable. 
+\end{proposition}
+\begin{proof}
+    Let $x \in E$, then there exists $\phi_x \in E^*$ such that $\dpn{x, \phi_x}{E} = \rho(x)$ and $|\phi_x| \le \rho$. Thus
+    \[
+    \rho(x) = \sup_{y \in E}\dpn{x, \phi_y}{E}
+    \]
+
+    is lower semicontinuous and Borel measurable by \autoref{proposition:semicontinuous-properties}. 
+\end{proof}
+