proposition: Lemma prod2_conv1_cont: continuous prod2_conv1 (Y:=ProductTopology2).
proof: Proof. apply pointwise_continuity. intros p. apply func_preserving_net_limits_is_continuous. intros. apply net_limit_in_projections_impl_net_limit_in_weak_topology. - destruct (H Full_set). + apply open_full. + constructor. + exact (inhabits x0). - destruct a; simpl. + now apply net_limit_in_weak_topology_impl_net_limit_in_projections with (a:=twoT_1) in H. + now apply net_limit_in_weak_topology_impl_net_limit_in_projections with (a:=twoT_2) in H. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)