Theorems · Theorem · general topology

exists_subset_iUnion_closure_subset

∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X],
  IsClosed s →
    (∀ (i : ι), IsOpen (u i)) →
      (∀ x ∈ s, {i | x ∈ u i}.Finite) →
        s ⊆ ⋃ i, u i → ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new open cover so that the closure of each new open set is contained in the corresponding original open set.

Defined in

Mathlib.Topology.ShrinkingLemma

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpace