proposition: Lemma continuity_1d_2d_pt_comp : forall f g x y, continuity_pt f (g x y) -> continuity_2d_pt g x y -> continuity_2d_pt (fun x y => f (g x y)) x y.
proof: Proof. intros f g x y Cf Cg. apply continuity_pt_filterlim in Cf. apply continuity_2d_pt_filterlim in Cg. apply continuity_2d_pt_filterlim. apply: filterlim_comp Cg Cf. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq