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

• rothberger {ι : Type u} (U : ℕ → ι → Set X) : Nonempty ι → (∀ (n : ℕ) (i : ι), IsOpen (U n i)) → (∀ (n : ℕ), Set.univ = ⋃ (i : ι), U n i) → ∃ (j : ℕ → ι), Set.univ = ⋃ (n : ℕ), U n (j n)