Updated nuclear spaces.

src/fa/lc/projective.tex

@@ -23,7 +23,7 @@
     By (U) of \autoref{definition:tvs-projective-limit} and \autoref{definition:tvs-initial}, $E$ is equipped with the projective topology generated by the projection maps $E \to E_i$. By \autoref{proposition:lc-projective-topology}, $E$ is locally convex.
 \end{proof}
 
-\begin{proposition}[{{\cite[II.5.4]{SchaeferWolff}}}]
+\begin{proposition}
 \label{proposition:complete-lc-projective-limit}
     Let $E$ be a separated complete locally convex space over $K \in \RC$, $\mathcal{B} \subset \cn_E(0)$ be a fundamental system of neighbourhoods consisting of convex, circled, and radial sets, directed under inclusion.
 
@@ -44,7 +44,7 @@
 
     \end{enumerate}
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[II.5.4]{SchaeferWolff}}}]
     (1): Since $V \supset U$, $[\cdot]_V \ge [\cdot]_U$, so $M_V \supset M_U$. Thus $\ker(\pi_V) \supset M_U$. By (U) of the \hyperref[quotient]{definition:tvs-quotient}, $\pi_V$ factors through $E_U$ as $\pi^U_V$, so $\pi^U_V \in L(E_U; E_V)$.
 
     (2): Since $\mathcal{B}$ is a fundamental system of neighbourhoods, it is downward-directed under inclusion. For any $U, V, W \in \mathcal{B}$ with $U \subset V \subset W$, $M_U \supset M_V \supset M_W$. Thus $\pi^U_W = \pi^V_W \circ \pi^U_V$.