From d59b4f69d3c4fb9761031a0db72bda88e199cae2 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sat, 26 Sep 2026 01:24:29 +0900
Subject: [PATCH] unif cont -> cont

---
 CHANGELOG_UNRELEASED.md                      |  3 +++
 theories/topology_theory/uniform_structure.v | 22 ++++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..d713debdf9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `uniform_structure.v`:
+  + lemma `unif_continuous_continuous`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 9169e8af18..b682c4f95a 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -328,6 +328,28 @@ Qed.
 Definition unif_continuous (U V : uniformType) (f : U -> V) :=
   (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.
 
+Lemma unif_continuous_continuous (U V : uniformType) (f : U -> V) :
+  unif_continuous f -> continuous f.
+Proof.
+move=> ucf /= u N fuN.
+have [V0 entV0 V0N] : exists2 V0 : set (V * V),
+    entourage V0 & xsection V0 (f u) `<=` N.
+  move: fuN; rewrite -filter_from_entourageE => -[V1 entV1 V1fuN].
+  by exists V1.
+have [U0 entU0 U0V0] : exists2 U0 : set (U * U),
+    entourage U0 & (fun x => (f x.1, f x.2)) @` U0 `<=` V0.
+  exists ((fun x => (f x.1, f x.2)) @^-1` V0).
+    exact: ucf.
+  by move=> [_ _]/= [x V0fx [<- <-]].
+have fU0uN : f @` (xsection U0 u) `<=` N.
+  move=> _/= [u0 U0u0 <-]; apply: V0N => /=.
+  by apply/mem_set/U0V0 => /=; exists (u, u0) => //=; exact/set_mem.
+apply/nbhsP; exists U0 => //.
+have := @preimage_subset _ _ f _ _ fU0uN.
+apply: subset_trans => u0/= U0uu0.
+by exists u0.
+Qed.
+
 Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) :=
   exists2 B, entourage B & forall PQ, A PQ -> forall p q,
     PQ.1 p -> PQ.2 q -> B (p,q).