English
If X is normal and U is a locally finite open cover of s, there exists f subordinate to U.
Русский
Если X нормальное, и U локально конечное открытое покрытие s, существует f, подчиненное U.
LaTeX
$$$$ \exists f : BumpCovering ι X s, f.IsSubordinate U. $$$$
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`. This version assumes that
`p : (X → ℝ) → Prop` is a predicate that satisfies Urysohn's lemma, and provides a
`BumpCovering` such that each function of the covering satisfies `p`. -/
theorem exists_isSubordinate_of_prop [NormalSpace X] [ParacompactSpace X] (p : (X → ℝ) → Prop)
(h01 :
∀ s t,
IsClosed s →
IsClosed t → Disjoint s t → ∃ f : C(X, ℝ), p f ∧ EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1)
(hs : IsClosed s) (U : ι → Set X) (ho : ∀ i, IsOpen (U i)) (hU : s ⊆ ⋃ i, U i) :
∃ f : BumpCovering ι X s, (∀ i, p (f i)) ∧ f.IsSubordinate U :=
by
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
rcases exists_isSubordinate_of_locallyFinite_of_prop p h01 hs V hVo hVf hsV with ⟨f, hfp, hf⟩
exact ⟨f, hfp, hf.mono hVU⟩
