proposition: Lemma weak_topology_is_weakest: forall (T':Family X) (H1:_) (H2:_) (H3:_), (forall a:A, continuous (f a) (X := Build_TopologicalSpace X T' H1 H2 H3)) -> forall U:Ensemble X, @open WeakTopology U -> T' U.
proof: Proof. intros. destruct H0. apply H1. intros. apply H0 in H4. induction H4. - exact H3. - destruct H4. apply H; trivial. - apply H2; trivial. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)