proposition: Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x : {for x, continuous f} <-> f @ x^' --> f x.
proof: Proof. split=> - cfx P /= fxP. by rewrite !near_simpl; apply: cvg_within; apply: cfx. 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]. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed