class PiBase.kω1Space (X : Type u_1) [TopologicalSpace X] : Prop

• k_omega : ∃ (K : ℕ → Set X), Monotone K ∧ Set.univ = ⋃ (n : ℕ), K n ∧ (∀ (n : ℕ), IsCompact (K n)) ∧ ∀ (s : Set X), IsOpen s ↔ ∀ (n : ℕ), IsOpen (Subtype.val ⁻¹' s)