proposition: Lemma weak_topology1_topology: forall U:Ensemble X, @open WeakTopology1 U <-> exists V:Ensemble Y, open V /\ U = inverse_image f V.
proof: Proof. split. 2: { intros. destruct H as [V []]. subst. apply weak_topology1_makes_continuous_func. assumption. } intros HU. exists (FamilyUnion (fun V : Ensemble Y => open V /\ Included (inverse_image f V) U)). split. { apply open_family_union. intros S [HS0 HS1]. assumption. } apply Extensionality_Ensembles; split; red. - assert (forall U:Ensemble X, In (finite_intersections (weak_topology_subbasis (True_rect f))) U -> exists V:Ensemble Y, open V /\ U = inverse_image f V). { clear U HU. intros U HU. induction HU. - exists Full_set. split. + apply open_full. + symmetry. apply inverse_image_full. - destruct H. destruct a. simpl. exists V. split; trivial. - destruct IHHU as [V1 [? ?]]. destruct IHHU0 as [V2 [? ?]]. exists (Intersection V1 V2). split. + auto with topology. + subst. symmetry. apply inverse_image_intersection. } intros x HUx. constructor. destruct HU. destruct HUx. specialize (H0 S H1). specialize (H S H0) as [V []]. subst. destruct H2. exists V; auto. split; auto. intros y Hy. exists (inverse_image f V); auto. - intros x HVx. destruct HVx. inversion H; subst; clear H. destruct H0. apply H0. constructor. assumption. Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)