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

• ex_seq (α : Type u) (s : α → Set X) : (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (ω : ℕ → Type u) (t : (n : ℕ) → ω n → Set X), (∀ (n : ℕ), (∀ (a : ω n), IsOpen (t n a)) ∧ ⋃ (a : ω n), t n a = Set.univ ∧ ∀ (b : ω n), ∃ (a : α), t n b ⊆ s a) ∧ ∀ (x : X), ∃ (n : ℕ), PointFiniteAt (t n) x