proposition: Lemma product2_map_continuous_at: forall (W:TopologicalSpace) (f:W -> X) (g:W -> Y) (w:W), continuous_at f w -> continuous_at g w -> continuous_at (fun w:W => (f w, g w)) w (Y:=ProductTopology2).
proof: Proof. intros. replace (fun w:W => (f w, g w)) with (fun w:W => prod2_conv1 (fun i:twoT => match i with | twoT_1 => f w | twoT_2 => g w end)). - apply (@continuous_composition_at W prod2 ProductTopology2 prod2_conv1 (fun w:W => fun i:twoT => match i with | twoT_1 => f w | twoT_2 => g w end)). + apply continuous_func_continuous_everywhere. apply prod2_conv1_cont. + apply product_map_continuous. now destruct a. - now extensionality w0. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)