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

• closure_refinement (α : Type u) (s : α → Set X) : (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (t : α → Set X), (∀ (a : α), IsOpen (t a)) ∧ ⋃ (a : α), t a = Set.univ ∧ ∀ (a : α), closure (t a) ⊆ s a