diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 47586cd04c..6d3bc729b0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,6 +11,8 @@
   + lemma `limn_einf_shift_new`
   + lemma `limn_einf_shiftS`
   + lemma `limn_einf_cst`
+- in `uniform_structure.v`:
+  + lemma `unif_continuous_continuous`
 
 ### Changed
 
diff --git a/classical/unstable.v b/classical/unstable.v
index 2045878059..7e3c2827f8 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -424,7 +424,7 @@ End reassociate_products.
 Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1).
 Proof. by case=> ? ?. Qed.
 
-Definition map_pair {S U : Type} (f : S -> U) (x : (S * S)) : (U * U) :=
+Definition map_pair {S U : Type} (f : S -> U) (x : S * S) : (U * U) :=
   (f x.1, f x.2).
 
 Section order_min.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 79719f209c..fbf94e28f7 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -299,7 +299,8 @@ have unif : unif_continuous (fun x => (0, x) : M * M).
   by rewrite inE/= => -[[[a1 a2] [b1 b2]]]/= /[swap]-[] -> -> <-.
 move=> /= U /sub_unif_continuous /unif /=.
 rewrite -comp_preimage/= /comp/= /nbhs/=.
-by congr entourage => /=; rewrite eqEsubset; split=> x /=; rewrite !sub0r.
+congr entourage => /=; rewrite eqEsubset.
+by split=> x; rewrite /map_pair/= !sub0r.
 Qed.
 
 Lemma add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2).
@@ -311,12 +312,12 @@ have unif: unif_continuous (fun x => (x.1, -x.2) : M * M).
       ((fun xy => (xy.1.1, xy.2.1, (-xy.1.2, -xy.2.2))) @^-1` (U1 `*` U2))).
     move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2.
     have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE.
-    by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-.
+    by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-.
   exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split.
   by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)).
 move=> /= U /sub_unif_continuous/unif; rewrite /nbhs/=.
 rewrite -comp_preimage/=/comp/=.
-by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !opprK.
+by congr entourage; rewrite eqEsubset; split=> x /=; rewrite /map_pair !opprK.
 Qed.
 
 HB.instance Definition _ :=
@@ -339,7 +340,7 @@ apply: (@filterS _ _ entourage_filter
     ((fun xy => (xy.1.1, xy.2.1, (- xy.1.2, - xy.2.2))) @^-1` (U1 `*` U2))).
   move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2.
   have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE.
-  by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-.
+  by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-.
 exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split.
 by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)).
 Qed.
@@ -374,11 +375,11 @@ have unif: unif_continuous (fun x => (-1, x) : R^o * M).
   have /U12 : ((-1, -1), x) \in U1 `*` U2.
     rewrite in_setX/= (mem_set xU2) andbT.
     by apply/mem_set; exact: entourage_refl.
-  by rewrite inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=.
+  by rewrite /map_pair inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=.
 move=> /= U /scale_unif_continuous/unif/=.
 rewrite /nbhs/=.
 rewrite -comp_preimage/=/comp/=.
-by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !scaleN1r.
+by congr entourage; rewrite eqEsubset; split=> x /=; rewrite /map_pair !scaleN1r.
 Qed.
 
 #[warning="-HB.no-new-instance"]
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 9169e8af18..caa36a3e54 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -1,6 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order algebra all_classical.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import topology_structure.
 
 (**md**************************************************************************)
@@ -326,7 +328,19 @@ by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhs_entourage.
 Qed.
 
 Definition unif_continuous (U V : uniformType) (f : U -> V) :=
-  (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.
+  (map_pair f) @ entourage --> entourage.
+
+Lemma unif_continuous_continuous (U V : uniformType) (f : U -> V) :
+  unif_continuous f -> continuous f.
+Proof.
+rewrite /unif_continuous /cvg_to !nbhs_simpl => ucf.
+rewrite /cvg_to /= => u X; rewrite !nbhs_simpl /= -!nbhs_entourageE.
+case => Y /ucf /=; set Y' := (Y' in entourage Y') => eY' YX.
+exists Y' => //.
+rewrite /Y' /=.
+rewrite -image_sub => v [] u' /= Yfuu' <-.
+exact: YX.
+Qed.
 
 Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) :=
   exists2 B, entourage B & forall PQ, A PQ -> forall p q,