toSmoothPartitionOfUnity_zero_of_zero

English

If the i-th bump function vanishes at a point x, then the i-th partition function vanishes at x as well.

Русский

Если i-й шип-функции принимает нуль в точке x, то и i-й элемент разбиения принимает нуль в этой точке.

LaTeX

$$$\\text{If } fs(i,x)=0, \\text{ then } fs.toSmoothPartitionOfUnity(i,x)=0.$$$

Lean4

theorem toSmoothPartitionOfUnity_zero_of_zero {i : ι} {x : M} (h : fs i x = 0) : fs.toSmoothPartitionOfUnity i x = 0 :=
  fs.toBumpCovering.toPartitionOfUnity_zero_of_zero h

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