toSmoothPartitionOfUnity_apply — Mathlib

English

For every i and x, the i-th function value equals φ_i(x) = φ_i(x) · ∏_{j ≺ i} (1 − φ_j(x)), where ≺ is the well-order relation used to order the index set.

Русский

Для каждого i и точки x значение функции i-го члена разбиения равно φ_i(x) = φ_i(x) · ∏_{j ≺ i} (1 − φ_j(x)), где ≺ обозначает лексикографический порядок индексов, задаваемый порядком.

LaTeX

$$$\\forall i, x:\\; \\phi_i(x) = \\phi_i(x) \\cdot \\prod_{j \\prec i} (1 - \\phi_j(x)).$$$

Lean4

theorem toSmoothPartitionOfUnity_apply (i : ι) (x : M) :
    fs.toSmoothPartitionOfUnity i x = fs i x * ∏ᶠ (j) (_ : WellOrderingRel j i), (1 - fs j x) :=
  rfl

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