diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f74d424376..675ff22b85 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,9 @@
 - in `num_normedtype.v`:
   + lemma `nbhs_infty_gtr`
 
+- in `uniform_structure.v`:
+  + lemma `continuous_injective_withinNx`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 611643c7da..51c439a410 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -284,6 +284,18 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
 Unshelve. all: by end_near. Qed.
 
+Lemma continuous_injective_withinNx
+  (T U : topologicalType) (f : T -> U) (x : T) :
+  {for x, continuous f} ->
+  (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'.
+Proof.
+move=> cf fI A; rewrite /nbhs /= /dnbhs !withinE/= => -[V Vfx AV].
+exists (f @^-1` V); first exact: cf Vfx.
+by apply/seteqP; split=> y/=;
+  move/predeqP : AV => /(_ (f y))/= AV [AVfy yx];
+  have /contra_neq /(_ yx) := fI y; tauto.
+Qed.
+
 (* This property is primarily useful for metrizability on uniform spaces *)
 Definition countable_uniformity (T : uniformType) :=
   exists R : set_system (T * T), [/\