toPartitionOfUnity_eq_mul_prod — Mathlib

English

The partition of unity equals the product-based expression; i.e., f.toPartitionOfUnity i x equals f i x times the finite product over j in t with WellOrderingRel j i of (1 − f j x).

Русский

Разложение по единице равно выражению через произведение; то есть f^{PartitionOfUnity}_i(x) = f_i(x) ⋅ ∏_{j∈t} (1 − f_j(x)).

LaTeX

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

Lean4

theorem toPartitionOfUnity_eq_mul_prod (i : ι) (x : X) (t : Finset ι)
    (ht : ∀ j, WellOrderingRel j i → f j x ≠ 0 → j ∈ t) :
    f.toPartitionOfUnity i x = f i x * ∏ j ∈ t with WellOrderingRel j i, (1 - f j x) :=
  f.toPOUFun_eq_mul_prod i x t ht

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