Theorems · Theorem · general topology

BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop

∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X] (p : (X → ℝ) → Prop),
  (∀ (s t : Set X),
      IsClosed s →
        IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) →
    IsClosed s →
      ∀ (U : ι → Set X),
        (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U

If X is a normal topological space and U i, i : ι, is a locally finite open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate. This version assumes that p : (X → ℝ) → Prop is a predicate that satisfies Urysohn's lemma, and provides a BumpCovering such that each function of the covering satisfies p.

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpace