Added bilinear forms.

src/fa/tvs/equicontinuous.tex

@@ -88,28 +88,6 @@
     and $\lambda(x_0, y - y_0) \in U$ as well. Therefore $\alg$ is equicontinuous at $(x_0, y_0)$. 
 \end{proof}
 
-
-
-\begin{theorem}
-\label{theorem:separate-joint-bilinear}
-    Let $E, F, G$ be TVSs over $K \in \RC$ and $\alg$ be separately continuous bilinear maps from $E \times F$ to $G$. If one of the following holds:
-    \begin{enumerate}
-        \item[(B)] $E$ is Baire.
-        \item[(B')] $E$ is barrelled and $G$ is locally convex. 
-    \end{enumerate}
-
-    and that
-    \begin{enumerate}
-        \item[(M)] $E$ and $F$ are both metrisable. 
-        \item[(E)] For each $x \in E$, $\bracsn{\lambda(x, \cdot)|\lambda \in \alg} \subset L(F; G)$ is equicontinuous. 
-    \end{enumerate}
-
-    then $\alg$ is equicontinuous. 
-\end{theorem}
-\begin{proof}[Proof, {{\cite[III.5.1]{SchaeferWolff}}}. ]
-    Let $\seq{(x_n, y_n)} \subset E \times F$ and $\seq{\lambda_n} \subset \alg$ such that $(x_n, y_n) \to 0$ as $n \to \infty$. Since $\seq{y_n}$ is convergent, for each $n \in \natp$ and $x \in E$, $\bracsn{\lambda_n(x, y_n)|n \in \natp}$ is bounded by (E) and \autoref{proposition:equicontinuous-net}. By (B) or (B') and the \hyperref[Banach-Steinhaus Theorem]{theorem:banach-steinhaus}, $\bracsn{\lambda_n(\cdot, y_n)|n \in \natp}$ is equicontinuous, and $\lambda_n(x_n, y_n) \to 0$ as $n \to \infty$ by \autoref{proposition:equicontinuous-net}. By (M) and \autoref{proposition:equicontinuous-net}, $\alg$ is equicontinuous at $0$, and hence equicontinuous by \autoref{lemma:equicontinuous-bilinear}. 
-\end{proof}
-
 % TODO: Replace this with a more general version involving polars in the future. 
 \begin{theorem}[Banach-Alaoglu]
 \label{theorem:alaoglu}