fact: Definition Lindelof_degree (X : TopologicalSpace) {Y : Type} (kappa : Ensemble Y) : Prop := least_cardinal (@Lindelof_degree_candidate X) kappa.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)