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

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