within_continuous_withinNx

Co-authored-by: mkerjean

Author: Tragicus

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,9 @@
 - in `num_normedtype.v`:
   + lemma `nbhs_infty_gtr`
 
+- in `uniform_structure.v`:
+  + lemma `within_continuous_withinNx`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:

theories/topology_theory/uniform_structure.v

@@ -284,6 +284,23 @@ 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 within_continuous_withinNx
+  (T U : topologicalType) (f : T -> U) (x : T) :
+  {for x, continuous f} ->
+  injective f -> f @ x^' --> (f x)^'.
+Proof.
+move=> cf fI A.
+rewrite /nbhs /= /dnbhs !withinE/= => -[] V Vfx AV.
+exists (f @^-1` V); first exact: (cf _ Vfx).
+apply/seteqP; split=> y/= [] fyAV yx; split=> //.
+  suff: f y \in A `&` (fun y : U => y != f x) by rewrite AV inE => -[].
+  rewrite inE/=; split=> //.
+  by move: yx; apply: contra => /eqP /fI /eqP.
+suff: f y \in V `&` (fun y : U => y != f x) by rewrite -AV inE => -[].
+rewrite inE/=; split=> //.
+by move: yx; apply: contra => /eqP /fI /eqP.
+Qed.
+
 (* This property is primarily useful for metrizability on uniform spaces *)
 Definition countable_uniformity (T : uniformType) :=
   exists R : set_system (T * T), [/\