sum_toSmoothPartitionOfUnity_eq — Mathlib

English

There exists a finite t such that equality holds as a neighborhood equality: the smooth partition equals a product expression restricted by t.

Русский

Существует конечное t, для которого равенство выполняется локально в окрестности точки.

LaTeX

$$$\\exists t \\ (fs.toSmoothPartitionOfUnity i =^\\!_{\\mathcal{N}_x} fs i \\cdot \\prod_{j \\in t} (1 - fs j))$$$

Lean4

theorem sum_toSmoothPartitionOfUnity_eq (x : M) : ∑ᶠ i, fs.toSmoothPartitionOfUnity i x = 1 - ∏ᶠ i, (1 - fs i x) :=
  fs.toBumpCovering.sum_toPartitionOfUnity_eq x

Похожие утверждения