proposition: Lemma second_countable_impl_separable: forall X:TopologicalSpace, second_countable X -> separable X.
proof: Proof. intros. destruct H as [B []]. destruct (choice (fun (U:{U:Ensemble X | In B U /\ Inhabited U}) (x:point_set X) => In (proj1_sig U) x)) as [choice_fun]. - intros. destruct x as [U [? ?]]. simpl. destruct i0. now exists x. - exists (Im Full_set choice_fun); split. + apply countable_img. red. match goal with |- CountableT ?S => pose (g := fun (x:S) => match x return {U:Ensemble X | In B U} with | exist (exist U (conj i _)) _ => exist _ U i end) end. apply inj_countable with g; trivial. red; intros x y H2. unfold g in H2. destruct x as [[U [? ?]]]. destruct y as [[V [? ?]]]. apply subset_eq, subset_eq. now injection H2. + apply meets_every_nonempty_open_impl_dense. intros. destruct H3, H. destruct (open_basis_cover x U) as [V [? [? ?]]]; trivial. assert (In B V /\ Inhabited V). { split; trivial. exists x; trivial. } exists (choice_fun (exist _ V H6)). constructor. * pose proof (H1 (exist _ V H6)). simpl in H7. exists (exist _ V H6). ** constructor. ** reflexivity. * apply H4. now pose proof (H1 (exist _ V H6)). Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)