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

• partition_refinement (α : Type u) (s : α → Set X) : (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (β : Type u) (t : β → Set X), (∀ (b : β), IsOpen (t b)) ∧ Setoid.IsPartition (Set.range t) ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a