Theorems · Theorem · general topology

precise_refinement_set

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

In a paracompact space, every open covering of a closed set admits a locally finite refinement indexed by the same type.

Defined in

Mathlib.Topology.Compactness.Paracompact

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceParacompactSpace