proposition: Lemma weak_topology1_topology_closed: forall U:Ensemble X, @closed WeakTopology1 U <-> exists V:Ensemble Y, closed V /\ U = inverse_image f V.
proof: Proof. unfold closed. split. - intros. unfold closed in *. rewrite weak_topology1_topology in H. destruct H as [V []]. exists (Complement V). rewrite inverse_image_complement. rewrite <- H0. rewrite !Complement_Complement. auto. - intros. destruct H as [V []]. subst. apply continuous_closed; try assumption. apply weak_topology1_makes_continuous_func. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)