class PiBase.KLindelofSpace (X : Type u) [TopologicalSpace X] : Prop

• ex_kSubcover {ι : Type u} {f : ι → TopologicalSpace.Opens X} (h : IsKCover f) : ∃ (ω : Type u) (g : ω → TopologicalSpace.Opens X), Countable ω ∧ IsKCover g ∧ Set.range g ⊆ Set.range f