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

• k_rothberger {ι : Type u} (U : ℕ → ι → Set X) : (∀ (n : ℕ), IsKCover'' (U n)) → ∃ (j : ℕ → ι), IsKCover'' fun (n : ℕ) => U n (j n)