sum_toPartitionOfUnity_eq — Mathlib

English

Summing the partition components yields 1 minus the product of (1 − f_i) over all indices.

Русский

Сумма компонент разложения по единице равна 1 минус произведение (1 − f_i) по всем индексам.

LaTeX

$$$\sum_i f^{\mathrm{PartitionOfUnity}}_i(x) = 1 - \prod_i (1 - f_i(x))$$$

Lean4

theorem sum_toPartitionOfUnity_eq (x : X) : ∑ᶠ i, f.toPartitionOfUnity i x = 1 - ∏ᶠ i, (1 - f i x) :=
  f.sum_toPOUFun_eq x

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