proposition: Lemma continuity_2d_pt_ext : forall f g x y, (forall x y, f x y = g x y) -> continuity_2d_pt f x y -> continuity_2d_pt g x y.
proof: Proof. intros f g x y Heq. apply continuity_2d_pt_ext_loc. apply locally_2d_locally. apply filter_forall. now intros [u v]. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq