toPartitionOfUnity_zero_of_zero

Mathlib.Topology.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#BumpCovering.toPartitionOfUnity_zero_of_zero

English

If f_i(x) = 0, then f.toPartitionOfUnity i x = 0.

Русский

Если f_i(x) = 0, то f^{PartitionOfUnity}_i(x) = 0.

LaTeX

$$$f_i(x) = 0 \implies f^{\mathrm{PartitionOfUnity}}_i(x) = 0$$$

Lean4

theorem toPartitionOfUnity_zero_of_zero {i : ι} {x : X} (h : f i x = 0) : f.toPartitionOfUnity i x = 0 :=
  f.toPOUFun_zero_of_zero h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru