English
In a paracompact normal space, for a predicate p and open cover U of s, there exists f subordinate to U with p(f_i) for all i.
Русский
В паркомпактном нормальном пространстве существует f, подчиненное U, и для всех i выполняется p(f_i).
LaTeX
$$$$ \exists f : BumpCovering ι X s, (\forall i, p(f_i)) \land f.IsSubordinate(U). $$$$
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_of_locallyFinite [NormalSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ i, IsOpen (U i))
(hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f : BumpCovering ι X s, f.IsSubordinate U :=
let ⟨f, _, hfU⟩ :=
exists_isSubordinate_of_locallyFinite_of_prop (fun _ => True)
(fun _ _ hs ht hd => (exists_continuous_zero_one_of_isClosed hs ht hd).imp fun _ hf => ⟨trivial, hf⟩) hs U ho hf
hU
⟨f, hfU⟩
