proposition: Lemma net_limit_in_projections_impl_net_limit_in_weak_topology : (forall a:A, net_limit (fun i:DS_set I => (f a) (x i)) ((f a) x0)) -> net_limit x x0.
proof: Proof. intros. red; intros. assert (@open_basis WeakTopology (finite_intersections weak_topology_subbasis)). { apply Build_TopologicalSpace_from_open_basis_basis. } destruct (open_basis_cover _ H2 x0 U) as [V [? [? ?]]]; trivial. assert (for large i:DS_set I, In V (x i)). { clear H4. induction H3. - destruct I_nonempty. exists X0; constructor. - destruct H3. destruct H5. apply eventually_impl_base with (fun i:DS_set I => In V (f a (x i))). + intros. constructor; trivial. + apply H; trivial. - apply eventually_impl_base with (fun i:DS_set I => In U0 (x i) /\ In V (x i)). + intros. destruct H6. constructor; trivial. + destruct H5. apply eventually_and; (apply IHfinite_intersections || apply IHfinite_intersections0); trivial. } refine (eventually_impl_base _ _ _ H6). intro; apply H4. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)