proposition: Lemma pointwise_continuity_2arg: (forall (x:X) (y:Y), continuous_at_2arg x y) -> continuous_2arg.
proof: Proof. intros. apply pointwise_continuity. intros [? ?]. apply H. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)