toPartitionOfUnity_apply — Mathlib

English

The partition of unity component equals the original bump function multiplied by the product over all preceding indices, i.e., the i-th component is f_i(x) times the product of (1 − f_j(x)) for j preceding i in the well-ordering.

Русский

Компонента разложения по единице равна f_i(x), умноженному на произведение (1 − f_j(x)) для всех j, предшествующих i в хорошо упорядоченном наборе.

LaTeX

$$$f^{\mathrm{POU}}_i(x) = f_i(x) \cdot \prod_{j} (1 - f_j(x))^{\text{with } WellOrderingRel(j,i)}$$$

Lean4

theorem toPartitionOfUnity_apply (i : ι) (x : X) :
    f.toPartitionOfUnity i x = f i x * ∏ᶠ (j) (_ : WellOrderingRel j i), (1 - f j x) :=
  rfl

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