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

• k_menger {ι : Type u} (U : ℕ → ι → Set X) : (∀ (n : ℕ), IsKCover'' (U n)) → ∃ (s : ℕ → Finset ι), IsKCover' {x : Set X | ∃ (n : ℕ) (i : ι) (_ : i ∈ s n), U n i = x}