From 39e967c1985c6d9e5404fe31f40458f3149b28b2 Mon Sep 17 00:00:00 2001
From: Bokuan Li <47512608+Jerry-licious@users.noreply.github.com>
Date: Thu, 8 Jan 2026 23:01:27 -0500
Subject: [PATCH] Reorganised the completion of uniform spaces.

---
 src/topology/uniform/cauchy.tex     |  0
 src/topology/uniform/complete.tex   | 18 ++++++++++++------
 src/topology/uniform/completion.tex |  4 ++--
 src/topology/uniform/index.tex      |  1 +
 4 files changed, 15 insertions(+), 8 deletions(-)
 create mode 100644 src/topology/uniform/cauchy.tex

diff --git a/src/topology/uniform/cauchy.tex b/src/topology/uniform/cauchy.tex
new file mode 100644
index 0000000..e69de29
diff --git a/src/topology/uniform/complete.tex b/src/topology/uniform/complete.tex
index de29d20..80f79cd 100644
--- a/src/topology/uniform/complete.tex
+++ b/src/topology/uniform/complete.tex
@@ -33,12 +33,18 @@
     Let $x \in X$ such that $\cn(x) \subset \fF$ and $V \in \fU$. By \ref{lemma:symmetricfundamentalentourage}, assume without loss of generality that $V \in \fU$. Since $\cn(x) \subset \fF$, then $V(x) \in \fU$ and $V(x) \times V(x) \subset V$.
 \end{proof}
 
+\begin{definition}[Cauchy Continuous]
+\label{definition:cauchy-continuous}
+    Let $X, Y$ be uniform spaces and $f: X \to Y$, then $f$ is \textbf{Cauchy continuous} if for any Cauchy filter base $\fB \subset 2^X$, $f(\fB) \subset 2^Y$ is Cauchy.
+\end{definition}
+
+
 \begin{proposition}[{{\cite[Proposition 2.3.3]{Bourbaki}}}]
 \label{proposition:imagecauchy}
-    Let $(X, \fU)$ and $(Y, \mathfrak{V})$ be uniform spaces, $f \in UC(X; Y)$, and $\fB \subset 2^X$ be a Cauchy filter base, then $f(\fB) \subset 2^Y$ is a Cauchy filter base.
+    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}
-    Let $V \in \mathfrak{V}$, then there exists $V' \in \fU$ such that $(f(x), f(y)) \in V$ whenever $(x, y) \in V'$. Given that $\fB$ is a Cauchy filter base, there exists $E \in \fB$ such that $E \times E \subset V'$, so $f(E) \times f(E) \subset V$.
+    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}
 
 \begin{definition}[Minimal Cauchy Filter]
@@ -131,7 +137,7 @@
     Let $X$ be a topological space, $Y$ be a complete Hausdorff uniform space, $A \subset X$ be a dense subset, and $f \in C(A; Y)$ be a continuous function, then the following are equivalent:
     \begin{enumerate}
         \item There exists a continuous function $F \in C(X; Y)$ such that $F|_A = f$.
-        \item For each $x \in X$, $f(\bracs{U \cap A| U \in \cn(x)})$ is a Cauchy filter base.
+        \item $f$ is Cauchy continuous.
     \end{enumerate}
 \end{proposition}
 \begin{proof}
@@ -141,10 +147,10 @@
 
 \begin{theorem}[Extension of Uniformly Continuous Functions, {{\cite[Theorem 1.3.2]{Bourbaki}}}]
 \label{theorem:uniform-continuous-extension}
-    Let $(X, \fU)$, $(Y, \fV)$ be uniform spaces, $A \subset Y$ be a dense subset, and $f \in UC(A; Y)$, then:
+    Let $(X, \fU)$ be a uniform space, $(Y, \fV)$ be a complete Hausdorff uniform space, $A \subset Y$ be a dense subset, and $f \in C(A; Y)$ be Cauchy continuous, then:
     \begin{enumerate}
-        \item There exists a unique $F \in UC(X; Y)$ such that $F|_A = f$.
-        \item $F \in UC(X; Y)$.
+        \item There exists a unique $F \in C(X; Y)$ such that $F|_A = f$.
+        \item If $f \in UC(A; Y)$, then $F \in UC(X; Y)$.
     \end{enumerate}
 \end{theorem}
 \begin{proof}
diff --git a/src/topology/uniform/completion.tex b/src/topology/uniform/completion.tex
index dce0efd..cb6dd29 100644
--- a/src/topology/uniform/completion.tex
+++ b/src/topology/uniform/completion.tex
@@ -8,7 +8,7 @@
     \begin{enumerate}
         \item $(\wh X, \wh \fU)$ is a complete Hausdorff uniform space.
         \item $\iota \in UC(X; \wh X)$.
-        \item[(U)] For any pair $(Y, f)$ satisfying (1) and (2), there exists unique $F \in C(\wh X; Y)$ such that the following diagram commutes
+        \item[(U)] For any complete Hausdorff uniform space $Y$ and Cauchy continuous function $f: X \to Y$, there exists unique $F \in C(\wh X; Y)$ such that the following diagram commutes
 
         \[
         \xymatrix{
@@ -17,7 +17,7 @@
         }
         \]
 
-        and $F \in UC(\wh X; Y)$.
+        Moreover, if $f \in UC(X; Y)$, then $F \in UC(\wh X; Y)$.
     \end{enumerate}
     Moreover,
     \begin{enumerate}
diff --git a/src/topology/uniform/index.tex b/src/topology/uniform/index.tex
index a3bb6a7..9001d95 100644
--- a/src/topology/uniform/index.tex
+++ b/src/topology/uniform/index.tex
@@ -3,5 +3,6 @@
 
 \input{./src/topology/uniform/definition.tex}
 \input{./src/topology/uniform/uc.tex}
+\input{./src/topology/uniform/cauchy.tex}
 \input{./src/topology/uniform/complete.tex}
 \input{./src/topology/uniform/completion.tex}