fact: Definition Lindelof_degree_candidate (X : TopologicalSpace) {Y : Type} (kappa : Ensemble Y) : Prop := forall cover : Family X, open_cover cover -> exists scover, subcover scover cover /\ le_cardinal_ens scover kappa.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)