English
There exists a smooth partition of unity subordinate to chartAt sources, i.e., subordinate to chart domains.
Русский
Существует гладкое разбиение единиц, подчинённое источникам chartAt.
LaTeX
$$$\\exists f: SmoothPartitionOfUnity, f.IsSubordinate (chartAt\\ H x).source$$$
Lean4
/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `SmoothPartitionOfUnity ι M s` that is subordinate to `U`. -/
theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (ho : ∀ i, IsOpen (U i))
(hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U :=
by
haveI : LocallyCompactSpace H := I.locallyCompactSpace
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
have := BumpCovering.exists_isSubordinate_of_prop (ContMDiff I 𝓘(ℝ) ∞) ?_ hs U ho hU
· rcases this with ⟨f, hf, hfU⟩
exact ⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩
· intro s t hs ht hd
rcases exists_smooth_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩
exact ⟨f, f.contMDiff, hf⟩
