proposition: Lemma continuous_localP {X Y : topologicalType} (f : X -> Y) : continuous f <-> forall (x : X), \forall U \near powerset_filter_from (nbhs x), {within U, continuous f}.
proof: Proof. split; first by move=> ? ?; near=> U; apply: continuous_subspaceT=> ?; exact. move=> + x => /(_ x)/near_powerset_filter_fromP. case; first by move=> ? ?; exact: continuous_subspaceW. move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U. move: nbhsU; rewrite nbhsE => -[] W [oW Wx WU] /(_ W). by move/(_ (continuous_subspaceW WU wctsf)); apply => //; exists W. move/nbhs_singleton: nbhsU; move: x; apply/in_setP. by rewrite -continuous_open_subspace. Unshelve. 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