Cleanup

src/fa/tvs/spaces-of-linear.tex

@@ -5,11 +5,12 @@
 \label{proposition:tvs-set-uniformity}
     Let $T$ be a set, $\mathfrak{S} \subset 2^T$ be an upward-directed system of sets, $F$ be a TVS over $K \in \RC$, then
     \begin{enumerate}
-        \item The $\mathfrak{S}$-uniformity on $F^T$ (\ref{definition:set-uniform}) is translation invariant.
+        \item The $\mathfrak{S}$-uniformity on $F^T$ (\autoref{definition:set-uniform}) is translation invariant.
         \item The composition defined by
         \[
         T^F \times T^F \to T^F \quad (f + g)(x) = f(x) + g(x)
         \]
+
         is continuous.
     \end{enumerate}
     For any vector subspace $\cf \subset F^T$, the following are equivalent:
@@ -19,7 +20,7 @@
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    (1): Let $U \subset F \times F$ be an entourage and $S \in \mathfrak{S}$. Using \ref{proposition:tvs-uniform}, assume without loss of generality that $U$ is translation-invariant. For any $(f, g) \in E(S, U)$, $h \in F^T$, and $x \in S$, $(f(x) + h(x), g(x) + h(x)) \in U$. Thus $(f + h, g + h) \in E(S, U)$ and $E(S, U)$ is translation-invariant.
+    (1): Let $U \subset F \times F$ be an entourage and $S \in \mathfrak{S}$. Using \autoref{proposition:tvs-uniform}, assume without loss of generality that $U$ is translation-invariant. For any $(f, g) \in E(S, U)$, $h \in F^T$, and $x \in S$, $(f(x) + h(x), g(x) + h(x)) \in U$. Thus $(f + h, g + h) \in E(S, U)$ and $E(S, U)$ is translation-invariant.
 
     (2): Let $f, g, f', g' \in \cf$, $S \in \mathfrak{S}$, and $U \subset F \times F$ be an entourage. By (TVS1), there exists an entourage $V \subset F \times F$ such that for any $x, x', y, y' \in F$ with $(x, x'), (y, y') \in V$, $(x + y, x' + y') \in U$. If $(f, g), (f', g') \in E(S, V) \cap \cf$, then for any $x \in S$, $(f(x) + g(x), f'(x) + g'(x)) \in U$, so $(f + g, f' + g') \in E(S, U) \cap \cf$.
 
@@ -30,10 +31,11 @@
     \lambda f(x) - \lambda' g(x) &= \lambda f(x) - \lambda' f(x) + \lambda' f(x) - \lambda' g(x) \\
     &= (\lambda - \lambda')f(x) + \lambda' (f(x) - g(x))
     \end{align*}
-    Let $U_0 \in \cn_F(0)$. By (TVS1) and \ref{proposition:tvs-good-neighbourhood-base}, there exists $U \in \cn_F(0)$ circled such that $U + U \subset U_0$. By (TVS2), there exists $V \in \cn_F(0)$ such that $\lambda' V \subset U$. Since $f(S)$ is bounded, there exists $\eps > 0$ with $\eps f(S) \subset U$. In which case, if $\abs{\lambda - \lambda'} < \eps$ and $f(x) - g(x) \in V$ for all $x \in S$, then
+    Let $U_0 \in \cn_F(0)$. By (TVS1) and \autoref{proposition:tvs-good-neighbourhood-base}, there exists $U \in \cn_F(0)$ circled such that $U + U \subset U_0$. By (TVS2), there exists $V \in \cn_F(0)$ such that $\lambda' V \subset U$. Since $f(S)$ is bounded, there exists $\eps > 0$ with $\eps f(S) \subset U$. In which case, if $\abs{\lambda - \lambda'} < \eps$ and $f(x) - g(x) \in V$ for all $x \in S$, then
     \[
     \lambda f(x) - \lambda' g(x) \in (\lambda - \lambda')f(S) + \lambda' V \subset U + U \subset U_0
     \]
+
     for all $x \in S$.
 \end{proof}
 
@@ -50,25 +52,30 @@
         \[
         I: B_{\mathfrak{S}}^k(E; B_{\mathfrak{S}}(E; F)) \to B^{k+1}_{\mathfrak{S}}(E; F)
         \]
+
         defined by
         \[
         (IT)(x_1, \cdots, x_{k+1}) = T(x_1, \cdots, x_k)(x_{k+1})
         \]
+
         is an isomorphism.
         \item The map
         \[
         I: \underbrace{B_{\mathfrak{S}}(E; B_{\mathfrak{S}}(E; \cdots)))}_{k \text{ times}} \to B^k_{\mathfrak{S}}(E; F)
         \]
+
         defined by
         \[
         IT(x_1, \cdots, x_k) = T(x_1)\cdots (x_k)
         \]
+
         is an isomorphism.
     \end{enumerate}
     which allows the identification
     \[
     \underbrace{B_{\mathfrak{S}}(E; B_{\mathfrak{S}}(E; \cdots)))}_{k \text{ times}} = B^k_{\mathfrak{S}}(E; F)
     \]
+
     under the map $I$ in (2).
 \end{proposition}
 \begin{proof}
@@ -76,10 +83,12 @@
     \[
     I^{-1}T: E \to B_{\mathfrak{S}}(E; F) \quad x \mapsto T(x, \cdot)
     \]
+
     Let $(x_1, \cdots, x_k) \in E^k$ and $S \in \mathfrak{S}$. Since $\mathfrak{S}$ is upward-directed and contains all singletons, assume without loss of generality that $\bracsn{x_j}_1^k \subset S$. In which case,
     \[
     T(x_1, \cdots, x_k, S) \subset T(S^{k+1}) \in B(F)
     \]
+
     by assumption. Thus $I^{-1}T(x_1, \cdots, x_k) \in B_{\mathfrak{S}}(E; F)$.
 
     In addition, for any $S_1 \in \mathfrak{S}$ and entourage $E(S_2, U)$ of $B_{\mathfrak{S}}(E; F)$ where $S_2 \in \mathfrak{S}$ and $U$ is an entourage of $F$, there exists $S \in \mathfrak{S}$ with $S \supset S_1 \cup S_2$. Given that $T(S^{k+1}) \in B(F)$, there exists $\lambda > 0$ such that $T(S^{k+1}) \subset \lambda U(0)$. In which case, $I^{-1}T(S^k) \subset \lambda E(S, U)(0)$ and $I^{-1}T(S^k) \in B(B_{\mathfrak{S}}(E; F))$. Thus $I^{-1}T \in B^k_{\mathfrak{S}}(E; B_{\mathfrak{S}}(E; F))$.
@@ -92,6 +101,7 @@
     \[
     \underbrace{B_{\mathfrak{S}}(E; B_{\mathfrak{S}}(E; \cdots)))}_{k+1 \text{ times}} = B^k_{\mathfrak{S}}(E; B_{\mathfrak{S}}(E; F)) = B^{k+1}_{\mathfrak{S}}(E; F)
     \]
+
     Thus (2) holds for all $k \in \natp$.
 \end{proof}