proposition: Lemma continuity_pt_ext_loc : forall f g x, locally x (fun x => f x = g x) -> continuity_pt f x -> continuity_pt g x.
proof: Proof. intros f g x Heq Cf. apply continuity_pt_filterlim in Cf. apply continuity_pt_filterlim. rewrite -(locally_singleton _ _ Heq). by apply filterlim_ext_loc with f. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq