proposition: Lemma first_countable_sequence_closure: forall (X:TopologicalSpace) (S:Ensemble X) (x:point_set X), first_countable X -> In (closure S) x -> exists y:Net nat_DS X, (forall n:nat, In S (y n)) /\ net_limit y x.
proof: Proof. intros. destruct (first_countable_open_neighborhood_bases _ H x) as [NB []]. destruct H2 as [g]. pose (U (n:nat) := IndexedIntersection (fun x: {x:{x:Ensemble X | In NB x} | (g x < n)%nat} => proj1_sig (proj1_sig x))). assert (forall n:nat, open (U n)). { intros. apply open_finite_indexed_intersection. - apply inj_finite with _ (fun x:{x:{x:Ensemble X | In NB x} | (g x < n)%nat} => exist (fun m:nat => (m<n)%nat) (g (proj1_sig x)) (proj2_sig x)). + apply finite_nat_initial_segment. + intros [[x0 P] p] [[y0 Q] q] ?. simpl in H3. apply subset_eq, subset_eq. simpl. injection H3; intros. apply H2 in H4. now injection H4. + intros; apply classic. - intros. destruct a as [[x0]]. now apply H1. } destruct (choice (fun (n:nat) (x:point_set X) => In (U n) x /\ In S x)) as [y]. - intros n. destruct (closure_impl_meets_every_open_neighborhood _ _ _ H0 (U n)) as [y]; trivial. + constructor; trivial. destruct a as [[x0]]. simpl. now apply H1. + exists y. destruct H4. now split. - exists y. split. + apply H4. + red; intros V ? ?. destruct H1. destruct (open_neighborhood_basis_cond V) as [W []]. * now split. * pose (a := (exist _ W H1 : {x:Ensemble X|In NB x})). exists (Datatypes.S (g a)). intros. simpl in j. simpl in H8. apply H7. assert (Included (U j) W). { red; intros. destruct H9. exact (H9 (exist _ a H8)). } apply H9, H4. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)