Added a few points about Cauchy completeness of metric spaces.

src/topology/metric/metric.tex

@@ -55,6 +55,20 @@
 \end{proof}
 
 
+\begin{proposition}
+\label{proposition:complete-metric-space}
+    Let $(X, d)$ be a metric space, then the following are equivalent:
+    \begin{enumerate}
+        \item For any Cauchy sequence $\seq{x_n} \subset X$, there exists $x \in X$ such that $x = \limv{n}x_n$. 
+        \item For any Cauchy sequence $\seq{x_n} \subset X$, there exists a subsequence $\seq{n_k}$ and $x \in X$ such that $x = \limv{k}x_{n_k}$. 
+        \item For every Cauchy filter $\fF \subset 2^X$, there exists $x \in X$ such that $\fF \to x$. 
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (2) $\Rightarrow$ (3): Since $\fF$ is Cauchy, there exists $\seq{E_n} \subset \fF$ such that for each $n \in \natp$, $E_n \supset E_{n+1}$ and $\sup_{y, z \in E_n}d(y, z) \le 1/n$. For each $n \in \natp$, let $x_n \in E_n$, then there exists a subsequence $\seq{n_k}$ and $x \in X$ such that $x = \limv{n}x_n$. In which case, $x \in \bigcap_{n \in \natp}\overline{E_n}$. For each $n \in \natp$, $\sup_{y, z\in E_n}d(y, z) \le 1/n$, so $B_X(x, 2/n) \supset E_n$. Therefore $\fF \to x$. 
+\end{proof}
+
+
 \begin{theorem}[Banach's Fixed Point Theorem]
 \label{theorem:banach-fixed-point}
     Let $(X, d)$ be a complete metric space and $f: X \to X$. If there exists $C \in (0, 1)$ such that

src/topology/uniform/cauchy.tex

@@ -54,11 +54,11 @@
 \end{definition}
 
 
-\begin{proposition}[{{\cite[Proposition 2.3.3]{Bourbaki}}}]
+\begin{proposition}
 \label{proposition:imagecauchy}
     Let $(X, \fU)$ and $(Y, \mathfrak{V})$ be uniform spaces and $f \in UC(X; Y)$, then $f$ is Cauchy continuous.
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Proposition 2.3.3]{Bourbaki}}}. ]
     Let $V \in \mathfrak{V}$, then there exists $V' \in \fU$ such that $(f(x), f(y)) \in V$ whenever $(x, y) \in V'$. For any Cauchy filter base $\fB \subset 2^X$, there exists $E \in \fB$ such that $E \times E \subset V'$, so $f(E) \times f(E) \subset V$.
 \end{proof}
 
@@ -67,7 +67,7 @@
     Let $X$ be a uniform space and $\fF \subset 2^X$ be a Cauchy filter, then $\fF$ is \textbf{minimal} if it is minimal with respect to inclusion.
 \end{definition}
 
-\begin{proposition}[{{\cite[Proposition 2.3.5]{Bourbaki}}}]
+\begin{proposition}
 \label{proposition:minimalcauchyexistence}
     Let $(X, \fU)$ be a uniform space and $\fF \subset 2^X$ be a Cauchy filter, then:
     \begin{enumerate}
@@ -75,7 +75,7 @@
         \item If $\fB \subset \fF$ is a base of $\fF$, and $\fV \subset \fU$ is a fundamental system of symmetric entourages, then $\mathfrak{M} = \bracs{V(M): V \in \fV, M \in \fB}$ is a base for $\fF_0$.
     \end{enumerate}
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Proposition 2.3.5]{Bourbaki}}}. ]
     Since $\fV$ and $\fB$ are both non-empty, $\mathfrak{M}$ is non-empty as well. Let $V_1, V_2 \in \fV$ and $M_1, M_2 \in \fB$. By (F2) of $\fV$ and $\fB$, there exists $V_0 \in \fV$ and $M_0 \in \fB$ such that $V_0 \subset V_1 \cap V_2$ and $M_0 \subset M_1 \cap M_2$. So $V_0(M_0) \subset V_1(M_1) \cap V_2(M_2)$, and $\mathfrak{M}$ satisfies (FB1). Given that $\emptyset \not\in \fV, \fB$, $\emptyset \not\in \mathfrak{M}$, so $\mathfrak{M}$ satisfies (FB2). By \autoref{proposition:filterbasecriterion}, $\mathfrak{M}$ is a filter base for
     \[
     \fF_0 = \bracs{E \subset X| \exists V \in \fV, M \in \fB: V(M) \subset E} \subset \fF
@@ -87,17 +87,17 @@
     Finally, let $\fF' \subset \fF$ be a Cauchy filter. Let $M \in \fB$ and $V \in \fV$, then there exists $N \in \fF'$ such that $N \times N \subset V$. Since $N \in \fF$, $M \cap N \ne \emptyset$, and there exists $y \in M \cap N$. For any $x \in N$, $N \times N \subset V$ implies that $x \in V(y)$. Hence $N \subset V(M)$ and $\fF' \supset \fF_0$.
 \end{proof}
 
-\begin{proposition}[{{\cite[Corollary 2.3.4]{Bourbaki}}}]
+\begin{proposition}
 \label{proposition:cauchyinterior}
     Let $(X, \fU)$ be a uniform space and $\fF \subset 2^X$ be a minimal Cauchy filter, then $\fF$ admits a base consisting of open sets.
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Corollary 2.3.4]{Bourbaki}}}. ]
     Let $\fV \subset \fU$ be the set of all symmetric, open entourages. By \autoref{proposition:goodentourages}, $\fV$ is a fundamental system of entourages. By \autoref{proposition:minimalcauchyexistence}, $\mathfrak{M} = \bracs{U(M)| U \in \fV, M \in \fF}$ is a base for $\fF$.
 
     Let $V \in \fU$, then there exists $U \in \fV$ such that $U \subset V$. For any $M \in \fF$, $U(M)$ is open by \autoref{lemma:openentourageneighbourhoods}. Thus $\mathfrak{M}$ consists of open sets.
 \end{proof}
 
-\begin{proposition}[{{\cite[Corollary 2.3.1, 2.3.2]{Bourbaki}}}]
+\begin{proposition}
 \label{proposition:cauchyfilterlimit}
     Let $(X, \fU)$ be a uniform space, then:
     \begin{enumerate}
@@ -106,7 +106,7 @@
         \item For any $x \in X$, filter $\fF \subset 2^X$ converging to $x$, and Cauchy filter $\mathfrak{G} \subset \fF$, $\mathfrak{G}$ converges to $x$.
     \end{enumerate}
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Corollary 2.3.1, 2.3.2]{Bourbaki}}}. ]
     (1): Let $\fF = \bracs{E \subset X: x \in E}$, then $\fF$ is a filter generated by the filter base $\fB = \bracs{\bracs{x}}$. By \autoref{proposition:minimalcauchyexistence}, $\bracs{U(x): U \in \fU} = \cn(x)$ is the unique minimal filter contained in $\fF$.
 
     (2): Let $x \in X$ be an accumulation point of $\fF$, then $U(x) \cap E \ne \emptyset$ for all $U \in \fU$ and $E \in \fF$. By \autoref{definition:generatedfilter}, there exists a filter $\fF' \supset \fF \cup \cn(x)$. Since $\fF$ is a Cauchy filter, so is $\fF'$. By minimality of $\cn(x)$, $\fF \supset \cn(x)$.