proposition: Lemma second_countable_impl_Lindelof: forall X:TopologicalSpace, second_countable X -> Lindelof X.
proof: Proof. intros. rewrite weight_second_countable_char in H. apply Lindelof_degree_Lindelof_char. destruct (Lindelof_degree_exists X) as [Y0 [kappa ?Hk]]. destruct (weight_exists X) as [lambda ?Hl]. pose proof (Lindelof_Lemma X kappa lambda Hk Hl). specialize (H (Ensemble X) lambda Hl). eapply Lindelof_degree_candidate_upwards_closed. 2: eapply H. eapply Lindelof_degree_candidate_upwards_closed. 2: eapply H0. apply Hk. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)