proposition: Lemma product_map_continuous: forall {A:Type} (X:TopologicalSpace) (Y:A->TopologicalSpace) (f:forall a:A, X -> Y a) (x:X), (forall a:A, continuous_at (f a) x) -> continuous_at (fun x:X => (fun a:A => f a x)) x (Y:=ProductTopology Y).
proof: Proof. intros. apply func_preserving_net_limits_is_continuous. intros. apply product_net_limit. - destruct (H0 Full_set) as [i]. + apply open_full. + constructor. + now exists. - intros. now apply continuous_func_preserves_net_limits. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)