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

• menger {ι : Type u} (U : ℕ → ι → Set X) : (∀ (n : ℕ) (i : ι), IsOpen (U n i)) → (∀ (n : ℕ), Set.univ = ⋃ (i : ι), U n i) → ∃ (s : ℕ → Finset ι), Set.univ = ⋃ (n : ℕ), ⋃ i ∈ s n, U n i