Theorems · Theorem · general topology

BumpCovering.exists_isSubordinate_of_prop

∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace 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)) → s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. 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

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceParacompactSpace