proposition: Theorem TychonoffProductTheorem: (forall a:A, compact (X a)) -> compact ProductTopology.
proof: Proof. intro. apply ultrafilter_limit_impl_compact. intros. destruct (choice_on_dependent_type (fun (a:A) (x:X a) => filter_limit (filter_direct_image (product_space_proj a) U) x)) as [choice_fun]. - intro. destruct (compact_impl_filter_cluster_point _ (H a) (filter_direct_image (product_space_proj a) U)) as [xa]. exists xa. apply ultrafilter_cluster_point_is_limit; trivial. red. intros. now destruct (H0 (inverse_image (product_space_proj a) S)); [left | right]; constructor; [ | rewrite inverse_image_complement ]. - exists choice_fun. now apply product_filter_limit. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)