English
In a normal space, given p on C(X,ℝ) and U open locally finite covering of s, there exists f subordinate to U with p on each f_i.
Русский
В нормальном пространстве существует подпокрытие f, подчинённое локально конечному открытому покрытию U, такое что f_i удовлетворяют свойству p.
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`. 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_locallyFinite_of_prop [NormalSpace 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)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) :
∃ f : BumpCovering ι X s, (∀ i, p (f i)) ∧ f.IsSubordinate U :=
by
rcases exists_subset_iUnion_closure_subset hs ho (fun x _ => hf.point_finite x) hU with ⟨V, hsV, hVo, hVU⟩
have hVU' : ∀ i, V i ⊆ U i := fun i => Subset.trans subset_closure (hVU i)
rcases exists_subset_iUnion_closure_subset hs hVo (fun x _ => (hf.subset hVU').point_finite x) hsV with
⟨W, hsW, hWo, hWV⟩
choose f hfp hf0 hf1 hf01 using fun i =>
h01 _ _ (isClosed_compl_iff.2 <| hVo i) isClosed_closure
(disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))
have hsupp : ∀ i, support (f i) ⊆ V i := fun i => support_subset_iff'.2 (hf0 i)
refine
⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1, fun i x => (hf01 i x).2,
fun x hx => ?_⟩,
hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i)⟩
rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩
exact ⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩
