fact: Definition Lindelof (X : TopologicalSpace) : Prop := forall cover:Family X, open_cover cover -> exists scover:Family X, subcover scover cover /\ Countable scover.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)