proposition: Corollary product2_map_continuous: forall (W:TopologicalSpace) (f:W -> X) (g:W -> Y), continuous f -> continuous g -> continuous (fun w:W => (f w, g w)) (Y:=ProductTopology2).
proof: Proof. intros. apply pointwise_continuity. intros. apply product2_map_continuous_at. - apply continuous_func_continuous_everywhere. assumption. - apply continuous_func_continuous_everywhere. assumption. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)