proposition: Lemma weak_topology_makes_continuous_funcs: forall a:A, continuous (f a) (X:=WeakTopology).
proof: Proof. intro. red; intros. pose proof (Build_TopologicalSpace_from_subbasis_subbasis _ weak_topology_subbasis). apply H0. constructor; trivial. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)