English
Let fs be a smooth bump covering on a smooth manifold M. Then there exists a smooth partition of unity {φ_i}_{i∈ι} subordinate to the covering, i.e., a family of smooth, nonnegative functions with supports contained in the corresponding bumps, whose sum is identically 1 on M.
Русский
Пусть fs — гладкое покрытие шипов на гладком многообразии M. Тогда существует гладкое разбиение единиц {φ_i}_{i∈ι}, подчинённое данному покрытию: множество гладких неотрицательных функций с опорой внутри соответствующих участков, сумма которых равна единице на M.
LaTeX
$$$\\exists (\\phi_i)_{i\\in \\iota},\\ \\forall i\\ \\phi_i \\in C^{\\infty}(M),\\ \\phi_i \\ge 0,\\ \\operatorname{supp}\\phi_i \\subset s,\\ \\sum_{i\\in \\iota} \\phi_i = 1 \\text{ on } M.$$$
Lean4
/-- Every `SmoothBumpCovering` defines a smooth partition of unity. -/
def toSmoothPartitionOfUnity : SmoothPartitionOfUnity ι I M s :=
fs.toBumpCovering.toSmoothPartitionOfUnity fun i => (fs i).contMDiff
