proposition: Lemma continuity_2d_pt_ext_loc : forall f g x y, locally_2d (fun u v => f u v = g u v) x y -> continuity_2d_pt f x y -> continuity_2d_pt g x y.
proof: Proof. intros f g x y Heq Cf. apply locally_2d_locally in Heq. apply continuity_2d_pt_filterlim in Cf. apply continuity_2d_pt_filterlim. rewrite -(locally_singleton _ _ Heq). apply filterlim_ext_loc with (2 := Cf). by apply Heq. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq