proposition: Lemma product_filter_limit: forall (F:Filter ProductTopology) (x0:ProductTopology), (forall a:A, filter_limit (filter_direct_image (product_space_proj a) F) (x0 a)) -> filter_limit F x0.
proof: Proof. intros F **. assert (subbasis (weak_topology_subbasis product_space_proj) (X:=ProductTopology)) by apply Build_TopologicalSpace_from_subbasis_subbasis. red. intros. red. intros U ?. destruct H1. destruct H1 as [U' []]. cut (In (filter_family F) U'). { intro. apply filter_upward_closed with U'; trivial. } destruct H1. destruct (subbasis_cover _ _ H0 _ _ H3 H1) as [V [? []]]. cut (In (filter_family F) V). { intro. eapply filter_upward_closed; eassumption. } clear U U' H1 H2 H3 H6. apply (filter_finite_intersection F (Intersection (weak_topology_subbasis product_space_proj) (fun U : Ensemble _ => In U x0))). 2: { clear F H H0. induction H5. - constructor. - constructor. split; auto. - destruct H4. intuition. apply intro_intersection; auto. } clear V H4 H5. intros b Hb. destruct Hb as [b Hb0 Hb1]. inversion Hb0; subst; clear Hb0. apply H. constructor. apply open_neighborhood_is_neighborhood. constructor; trivial. apply Hb1. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)