English
In a locally compact T2 space, given p on X → ℝ and a local finite cover with Urysohn property, there exists f subordinate with p and HasCompactSupport.
Русский
В локально компактном T2-пространстве существует подпокрытие с свойством p и компактной опорой.
LaTeX
$$$$ \exists f : BumpCovering ι X s, (\forall i, p (f_i)) \land f.IsSubordinate U \land \forall i, HasCompactSupport (f_i). $$$$
Lean4
/-- If `X` is a locally compact T2 topological space and `U i`, `i : ι`, is a locally finite open
covering of a compact 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_t2space [LocallyCompactSpace X] [T2Space X] (p : (X → ℝ) → Prop)
(h01 :
∀ s t,
IsClosed s →
IsCompact t → Disjoint s t → ∃ f : C(X, ℝ), p f ∧ EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1)
(hs : IsCompact 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 ∧ ∀ i, HasCompactSupport (f i) :=
by
rcases exists_subset_iUnion_closure_subset_t2space hs ho (fun x _ => hf.point_finite x) hU with
⟨V, hsV, hVo, hVU, hcp⟩
have hVU' i : V i ⊆ U i := subset_closure.trans (hVU i)
rcases exists_subset_iUnion_closure_subset_t2space hs hVo (fun x _ => (hf.subset hVU').point_finite x) hsV with
⟨W, hsW, hWo, hWV, hWc⟩
choose f hfp hf0 hf1 hf01 using fun i =>
h01 _ _ (isClosed_compl_iff.2 <| hVo i) (hWc i) (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))
have hsupp i : support (f i) ⊆ V 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), fun i =>
IsCompact.of_isClosed_subset (hcp i) isClosed_closure <| closure_mono (hsupp 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)⟩
