proposition: Lemma prod2_conv2_cont: continuous prod2_conv2 (X:=ProductTopology2).
proof: Proof. apply pointwise_continuity. destruct x as [x y]. 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 x1). - destruct a. + unfold product_space_proj. simpl. replace (fun i => prod2_conv2 (x0 i) twoT_1) with (fun i => fst (x0 i)). * now apply net_limit_in_weak_topology_impl_net_limit_in_projections with (a:=twoT_1) in H. * extensionality i. now destruct (x0 i). + unfold product_space_proj. simpl. replace (fun i:DS_set I => prod2_conv2 (x0 i) twoT_2) with (fun i:DS_set I => snd (x0 i)). * now apply net_limit_in_weak_topology_impl_net_limit_in_projections with (a:=twoT_2) in H. * extensionality i. now destruct (x0 i). Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)