proposition: Lemma weak_topology_continuous_char (W : TopologicalSpace) (g : W -> WeakTopology) : continuous g <-> (forall a, continuous (compose (f a) g)).
proof: Proof. split. - intros. unfold compose. apply continuous_composition. + apply weak_topology_makes_continuous_funcs. + assumption. - intros. apply continuous_subbasis with weak_topology_subbasis. { apply Build_TopologicalSpace_from_subbasis_subbasis. } intros. induction H0. rewrite <- inverse_image_composition. apply H. assumption. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)