English
The finite sum (finsum) of the partition components equals a specified combination of the φ_i, matching the standard unity partition identity.
Русский
Сумма функций разбиения даёт идентичность, приравнивающую к единице на многообразии.
LaTeX
$$$\\sum_{i} \\phi_i(x) = 1$ for all x in M.$$
Lean4
/-- Given two disjoint closed sets `s, t` in a Hausdorff σ-compact finite-dimensional manifold,
there exists an infinitely smooth function that is equal to `0` on `s` and to `1` on `t`.
See also `exists_msmooth_zero_iff_one_iff_of_isClosed`, which ensures additionally that
`f` is equal to `0` exactly on `s` and to `1` exactly on `t`. -/
theorem exists_smooth_zero_one_of_isClosed [T2Space M] [SigmaCompactSpace M] {s t : Set M} (hs : IsClosed s)
(ht : IsClosed t) (hd : Disjoint s t) : ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc 0 1 :=
by
have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd hx)
rcases SmoothBumpCovering.exists_isSubordinate I ht this with ⟨ι, f, hf⟩
set g := f.toSmoothPartitionOfUnity
refine ⟨⟨_, g.contMDiff_sum⟩, fun x hx => ?_, fun x => g.sum_eq_one, fun x => ⟨g.sum_nonneg x, g.sum_le_one x⟩⟩
suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
refine fun i => f.toSmoothPartitionOfUnity_zero_of_zero ?_
exact notMem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)
