proposition: Lemma Lindelof_degree_Lindelof_char (X : TopologicalSpace) : Lindelof X <-> Lindelof_degree_candidate X (@Full_set nat).
proof: Proof. unfold Lindelof, Lindelof_degree_candidate. split. - intros ? cover Hcover. specialize (H cover Hcover) as [scover [? ?]]. exists scover. split; try assumption. apply Countable_as_le_cardinal_ens. assumption. - intros ? cover Hcover. specialize (H cover Hcover) as [scover []]. exists scover. repeat split; try apply H. apply Countable_as_le_cardinal_ens. assumption. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)