toPOUFun_zero_of_zero

Mathlib.Topology.PartitionOfUnity

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

English

If f_i(x) = 0, then g_i(x) = 0 in the partition of unity.

Русский

Если f_i(x) = 0, то g_i(x) = 0 в разбиении единиц.

LaTeX

$$$$ f_i(x) = 0 \Rightarrow g_i(x) = 0. $$$$

Lean4

theorem toPOUFun_zero_of_zero {i : ι} {x : X} (h : f i x = 0) : f.toPOUFun i x = 0 := by rw [toPOUFun, h, zero_mul]

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

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

Разделы

Аффилиация

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