English
There exists a smooth partition subordinate to a locally finite cover by closed sets K_i and open sets U_i.
Русский
Существует гладкое разбиение единиц, подчинённое локально конечному покрытию из замкнутых K_i и открытых U_i.
LaTeX
$$$\\exists δ: SmoothPartitionOfUnity, δ.IsSubordinate (i\\mapsto U_i)$$$
Lean4
/-- Let `M` be a smooth σ-compact manifold with a metric. Let `K : ι → Set M` be a locally finite
family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for all
`i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and `x ∈ K i`,
we have `Metric.closedBall x (δ x) ⊆ U i`. -/
theorem exists_smooth_forall_closedBall_subset {M} [MetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
[SigmaCompactSpace M] {K : ι → Set M} {U : ι → Set M} (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i))
(hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
∃ δ : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯, (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i :=
by
rcases Emetric.exists_smooth_forall_closedBall_subset I hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
refine ⟨δ, hδ0, fun i x hx => ?_⟩
rw [← Metric.emetric_closedBall (hδ0 _).le]
exact hδ i x hx
