Generalise continuous_withinNx

Author: drouhling

CHANGELOG_UNRELEASED.md

@@ -60,6 +60,8 @@
   + `completeType` inherits from `uniformType` and not from `pseudoMetricType`
   + lemmas `close_trans`, `close_cvgxx`, `cvg_closeP` and `close_cluster` are
     valid for a `uniformType`
+  + moved `continuous_withinNx` from `normedType.v` to `topology.v` and
+    generalised it to `uniformType`
 
 ### Renamed
 

theories/normedtype.v

@@ -4196,20 +4196,6 @@ Lemma continuity_ptE (f : Rdefinitions.R -> Rdefinitions.R) (x : Rdefinitions.R)
   Ranalysis1.continuity_pt f x <-> {for x, continuous f}.
 Proof. exact: continuity_pt_cvg. Qed.
 
-Lemma continuous_withinNx (R : numFieldType) {U V : pseudoMetricType R}
-  (f : U -> V) x :
-  {for x, continuous f} <-> f @ nbhs' x --> f x.
-Proof.
-split=> - cfx P /= fxP.
-  rewrite /nbhs' !near_simpl near_withinE.
-  by rewrite /nbhs'; apply: cvg_within; apply/cfx.
- (* :BUG: ssr apply: does not work,
-    because the type of the filter is not inferred *)
-rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP.
-rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
-by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
-Grab Existential Variables. all: end_near. Qed.
-
 Lemma continuity_pt_cvg' f x :
   Ranalysis1.continuity_pt f x <-> f @ nbhs' x --> f x.
 Proof. by rewrite continuity_ptE continuous_withinNx. Qed.

theories/topology.v

@@ -2855,6 +2855,19 @@ Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core.
 Arguments entourage_split {M} z {x y A}.
 Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core.
 
+Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x :
+  {for x, continuous f} <-> f @ nbhs' x --> f x.
+Proof.
+split=> - cfx P /= fxP.
+  rewrite /nbhs' !near_simpl near_withinE.
+  by rewrite /nbhs'; apply: cvg_within; apply/cfx.
+ (* :BUG: ssr apply: does not work,
+    because the type of the filter is not inferred *)
+rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP.
+rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
+by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
+Grab Existential Variables. all: end_near. Qed.
+
 Section uniform_closeness.
 
 Variable (U : uniformType).