Theorems · Theorem · general topology

precise_refinement

∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] [ParacompactSpace X] (u : ι → Set X),
  (∀ (a : ι), IsOpen (u a)) →
    ⋃ i, u i = Set.univ → ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = Set.univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Any open cover of a paracompact space has a locally finite precise refinement, that is, one indexed on the same type with each open set contained in the corresponding original one.

Defined in

Mathlib.Topology.Compactness.Paracompact

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceParacompactSpace