Theorems · Theorem · general topology

exists_iUnion_eq_closure_subset

∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} [NormalSpace X],
  (∀ (i : ι), IsOpen (u i)) →
    (∀ (x : X), {i | x ∈ u i}.Finite) →
      ⋃ i, u i = Set.univ → ∃ v, Set.iUnion v = Set.univ ∧ (∀ (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

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpace