proposition: Lemma weak_topology1_continuous_char (Z : TopologicalSpace) (g : Z -> WeakTopology1) : continuous g <-> continuous (compose f g).
proof: Proof. replace f with (True_rect f I). 2: { reflexivity. } unfold WeakTopology1. rewrite weak_topology_continuous_char. split; intros; auto. destruct a. assumption. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)