Housekeeping.

src/fa/norm/normed.tex

@@ -10,8 +10,44 @@
         \item[(SN2)] For any $x \in E$ and $\lambda \in K$, $\norm{\lambda x}_E = \abs{\lambda} \norm{x}_E$.
         \item[(SN3)] For any $x, y \in E$, $\norm{x + y}_E \le \norm{x}_E + \norm{y}_E$.
     \end{enumerate}
+
+    In which case, the pair $(E, \norm{\cdot}_E)$ is a \textbf{normed vector space} over $K$. 
 \end{definition}
 
+\begin{definition}[Banach Space]
+\label{definition:banach-space}
+    Let $E$ be a normed vector space over $K \in \RC$, then $E$ is a \textbf{Banach space} if it is complete. 
+\end{definition}
+
+\begin{lemma}
+\label{lemma:banach-criterion}
+    Let $E$ be a normed vector space, then the following are equivalent:
+    \begin{enumerate}
+        \item $E$ is a Banach space.
+        \item For each $\seq{x_n} \subset E$ with $\sum_{n \in \natp}\norm{x_n}_E < \infty$, there exists $x \in E$ such that $x = \sum_{n = 1}^\infty x_n$. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (2) $\Rightarrow$ (1): Let $\seq{x_n} \subset E$ be a Cauchy sequence, then there exists a subsequence $\seq{n_k}$ such that $\norm{x_{n_{k+1}} - x_{n_{k}}}_E < 2^{-k}$ for all $k \in \natp$. For each $k \in \natp$, let $y_k = x_{n_{k+1}} - x_{n_{k}}$, then there exists $y \in E$ such that $y = \sum_{k = 1}^\infty y_k$. Let $\eps > 0$, then there exists $K \in \natp$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item $\norm{y - \sum_{k = 1}^{K-1} y_k}_E < \eps$. 
+        \item For each $n \ge n_K$, $\norm{x_n - x_{n_K}}_E < \eps$. 
+    \end{enumerate}
+
+    In which case, for every $n \ge n_K$, 
+    \begin{align*}
+        \norm{x_n - (y + x_{n_1})}_E &< \norm{x_{n_K} - (y + x_{n_1})}_E + \eps \\
+        &= \norm{y - \sum_{k = 1}^{K-1} (x_{n_{k+1}} - x_{n_{k}})}_E + \eps \\
+        &= \norm{y - \sum_{k = 1}^{K-1} y_k}_E + \epsilon < 2\eps
+    \end{align*}
+
+    Therefore $x_n \to y + x_{n_1}$ as $n \to \infty$. 
+    
+    
+\end{proof}
+
+
+
 \begin{proposition}
 \label{proposition:norm-criterion}
     Let $E$ be a separated TVS over $K \in \RC$, then the following are equivalent: