English
The i-th component of the partition of unity equals the original bump function value times a finite product of (1 − f_j) over a finite set t, under a conditioning that ensures the factors are nonzero only for those j in t that precede i in a well-order.
Русский
i-я компонента разложения по единице равна f_i(x) умножить на конечный произведение (1 − f_j(x)) по j из конечного множества t, при условии, что применяются только те j, которые precede i в хорошо упорядоченном наборе.
LaTeX
$$$f^{\mathrm{POU}}_i(x) = f_i(x) \cdot \prod_{j \in t \text{ with } WellOrderingRel(j,i)} (1 - f_j(x))$$$
Lean4
theorem toPOUFun_eq_mul_prod (i : ι) (x : X) (t : Finset ι) (ht : ∀ j, WellOrderingRel j i → f j x ≠ 0 → j ∈ t) :
f.toPOUFun i x = f i x * ∏ j ∈ t with WellOrderingRel j i, (1 - f j x) :=
by
refine congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)
rw [Ne, sub_eq_self] at hj
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]
exact flip (ht j) hj
