English
In a normal paracompact space, there exists a bump covering subordinate to an open cover, with compact support for each piece.
Русский
В нормальном паркомпактном пространстве существует BumpCovering, подчиненное открытому покрытию, с компактной опорой каждого элемента.
LaTeX
$$$$ \exists f : BumpCovering ι X s, f.IsSubordinate U \land \forall i, HasCompactSupport (f_i). $$$$
Lean4
/-- If `X` is a normal topological space and `U i`, `i : ι`, is a locally finite open covering of a
closed set `s`, then there exists a `BumpCovering ι 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_hasCompactSupport_of_locallyFinite_t2space [LocallyCompactSpace X] [T2Space X]
(hs : IsCompact s) (U : ι → Set X) (ho : ∀ i, IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) :
∃ f : BumpCovering ι X s, f.IsSubordinate U ∧ ∀ i, HasCompactSupport (f i) := by
-- need to switch 0 and 1 in `exists_continuous_zero_one_of_isCompact`
simpa using
exists_isSubordinate_of_locallyFinite_of_prop_t2space (fun _ => True)
(fun _ _ ht hs hd => (exists_continuous_zero_one_of_isCompact' hs ht hd.symm).imp fun _ hf => ⟨trivial, hf⟩) hs U
ho hf hU
