English
In a normal space, given a closed set s and an open cover U of s which is locally finite, there exists a partition of unity f subordinate to U.
Русский
В нормальном пространстве, для замыкания s и открытого покрытия U ветви U локально скольких элементов, существует разложение по единице, подпадающее под U.
LaTeX
$$$[NormalSpace X] \; IsClosed\ s \to \; \exists f:\ PartitionOfUnity\ ι\ X\ s,\; f.IsSubordinate U$$$
Lean4
/-- 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`. -/
theorem exists_isSubordinate_of_locallyFinite [NormalSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ i, IsOpen (U i))
(hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f : PartitionOfUnity ι X s, f.IsSubordinate U :=
let ⟨f, hf⟩ := BumpCovering.exists_isSubordinate_of_locallyFinite hs U ho hf hU
⟨f.toPartitionOfUnity, hf.toPartitionOfUnity⟩
