English
If f is a SmoothBumpCovering subordinate to U, then f.IsSubordinate U holds as a property of the bump covering.
Русский
Если f является SmoothBumpCovering, подчинённым U, то у него выполняется подчинённость f(IsSubordinate) U.
LaTeX
$$f.IsSubordinate U$$
Lean4
/-- Let `M` be a smooth manifold modelled on a finite-dimensional real vector space.
Suppose also that `M` is a Hausdorff `σ`-compact topological space. Let `s` be a closed set
in `M` and `U : M → Set M` be a collection of sets such that `U x ∈ 𝓝 x` for every `x ∈ s`.
Then there exists a smooth bump covering of `s` that is subordinate to `U`. -/
theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate U := by
-- First we deduce some missing instances
haveI : LocallyCompactSpace H := I.locallyCompactSpace
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
have hB := fun x hx => SmoothBumpFunction.nhds_basis_support (I := I) (hU x hx)
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with ⟨ι, c, f, hf, hsub', hfin⟩
choose hcs hfU using hf
rcases
exists_subset_iUnion_closed_subset hs (fun i => (f i).isOpen_support) (fun x _ => hfin.point_finite x) hsub' with
⟨V, hsV, hVc, hVf⟩
choose r hrR hr using fun i => (f i).exists_r_pos_lt_subset_ball (hVc i) (hVf i)
refine ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun i => ?_⟩
· simpa only [SmoothBumpFunction.support_updateRIn]
· refine (mem_iUnion.1 <| hsV hx).imp fun i hi => ?_
exact ((f i).updateRIn _ _).eventuallyEq_one_of_dist_lt ((f i).support_subset_source <| hVf _ hi) (hr i hi).2
· simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i
