proposition: Lemma second_countable_impl_first_countable: forall X:TopologicalSpace, second_countable X -> first_countable X.
proof: Proof. intros. destruct H as [B []]. red; intros. exists [ U:Ensemble X | In B U /\ In U x ]; split. - apply open_neighborhood_basis_is_neighborhood_basis. apply open_basis_to_open_neighborhood_basis; trivial. - apply countable_downward_closed with B; trivial. red; intros. now destruct H1 as [[? ?]]. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)