proposition: Lemma ProductTopology2_basis_is_basis: open_basis ProductTopology2_basis.
proof: Proof. assert (open_basis (finite_intersections (weak_topology_subbasis prod2_proj)) (X:=ProductTopology2)) by apply Build_TopologicalSpace_from_open_basis_basis. apply eq_ind with (1:=H). apply Extensionality_Ensembles; split; red; intros U ?. - induction H0. + rewrite <- EnsembleProduct_Full. constructor; apply open_full. + destruct H0. destruct a. * simpl. rewrite inverse_image_fst. constructor; auto with topology. * simpl. rewrite inverse_image_snd. constructor; auto with topology. + destruct IHfinite_intersections as [U1 V1]. destruct IHfinite_intersections0 as [U2 V2]. rewrite EnsembleProduct_Intersection. constructor; auto with topology. - destruct H0. rewrite EnsembleProduct_proj. constructor 3. + constructor. replace (@fst X Y) with (prod2_proj twoT_1); auto. constructor. assumption. + constructor. replace (@snd X Y) with (prod2_proj twoT_2); auto. constructor. assumption. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)