English
If X is locally compact and T2, and s is compact, then given an open cover U with locally finite property, there exists a partition of unity subordinate to U with each component having compact support.
Русский
Если X локально компактно и точечно, а s компактно, существует разложение по единице подпадающее под локально подобранное открытое покрытие U, компоненты которого имеют компактную опору.
LaTeX
$$[LocallyCompactSpace X] [T2Space X] → IsCompact s → (U : ι → Set X) → (ho : ∀ i, IsOpen (U i)) → LocallyFinite U → (hU : s ⊆ ⋃ i, U i) → ∃ f : PartitionOfUnity ι X s, f.IsSubordinate U ∧ ∀ i, HasCompactSupport (f i)$$
Lean4
/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `PartitionOfUnity ι X s` that is subordinate to `U`. -/
theorem exists_isSubordinate [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ι → Set X)
(ho : ∀ i, IsOpen (U i)) (hU : s ⊆ ⋃ i, U i) : ∃ f : PartitionOfUnity ι X s, f.IsSubordinate U :=
let ⟨f, hf⟩ := BumpCovering.exists_isSubordinate hs U ho hU
⟨f.toPartitionOfUnity, hf.toPartitionOfUnity⟩
