proposition: Lemma product_net_limit: forall (I:DirectedSet) (x:Net I ProductTopology) (x0:ProductTopology), inhabited (DS_set I) -> (forall a:A, net_limit (fun i:DS_set I => x i a) (x0 a)) -> net_limit x x0.
proof: Proof. intros. now apply net_limit_in_projections_impl_net_limit_in_weak_topology. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)