proposition: Lemma net_limit_in_weak_topology_impl_net_limit_in_projections : net_limit x x0 -> forall a:A, net_limit (fun i:DS_set I => (f a) (x i)) ((f a) x0).
proof: Proof. intros. apply continuous_func_preserves_net_limits; trivial. apply continuous_func_continuous_everywhere. apply weak_topology_makes_continuous_funcs. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)