English
In a locally compact T2 space, for a compact s, there exists f subordinate to U with each f_i having compact support.
Русский
В локально компактном T2-пространстве для компактного s существует подпокрытие f с компактной опорой каждой f_i.
LaTeX
$$$$ \exists f : BumpCovering ι X s, f.IsSubordinate U \land \forall 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 `BumpCovering ι 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 : BumpCovering ι X s, f.IsSubordinate U :=
by
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩
exact ⟨f, hf.mono hVU⟩
