proposition: Lemma near_cst_continuous (T U : topologicalType) (l : U) (f : T -> U) (x : T) : (\forall y \near x, f y = l) -> {for x, continuous f}.
proof: Proof. move=> eq_f_l; apply: cvg_near_cst; apply: filterS (eq_f_l) => y ->. by rewrite (nbhs_singleton eq_f_l). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed