proposition: Lemma continuous_ext_loc (f g : T -> U) (x : T) : locally x (fun y : T => g y = f y) -> continuous g x -> continuous f x.
proof: Proof. intros. eapply filterlim_ext_loc. by apply H. by rewrite -(locally_singleton _ _ H). Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq