Theorems · Theorem · general topology

PartitionOfUnity.exists_isSubordinate_of_locallyFinite

∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X],
  IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U

If X is a normal topological space and U is a locally finite open covering of a closed set s, then there exists a PartitionOfUnity ι 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.

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpace