class PiBase.SigmaRelativelyCompactSpace (X : Type u_1) [TopologicalSpace X] : Prop

• sigma_relatively_compact : ∃ (R : ℕ → Set X), ⋃ (n : ℕ), R n = Set.univ ∧ ∀ (n : ℕ), IsRelativelyCompact (R n)