proposition: Lemma continuity_pt_ext : forall f g x, (forall x, f x = g x) -> continuity_pt f x -> continuity_pt g x.
proof: Proof. intros f g x Heq. apply continuity_pt_ext_loc. by apply filter_forall. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq