English
For a multilinear map f and constant elements x, y in the target modules, the curryFinFinset construction yields the equality between the value of the curried map on the constants and the original map applied to the piecewise-constant combination built from x and y over the split indices.
Русский
Для много-линейной карты f и константных элементов x, y в целевых модулях, конструкция curryFinFinset дает равенство между значением затащенного отображения на константах и исходной карты примененной к разбиению по индексам с кусочно-константным объединением x и y.
LaTeX
$$$\bigl(\mathrm{curryFinFinset}\; R \; M_2 \; M' \ hk \ hl \; f \; (\lambda _ . x) \; (\lambda _ . y)\bigr) = f\bigl( s.\mathrm{piecewise}(\lambda _ . x) (\lambda _ . y) \bigr).$$$
Lean4
theorem curryFinFinset_apply_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
(f : MultilinearMap R (fun _ : Fin n => M') M₂) (x y : M') :
(curryFinFinset R M₂ M' hk hl f (fun _ => x) fun _ => y) = f (s.piecewise (fun _ => x) fun _ => y) := by
rw [← curryFinFinset_symm_apply_piecewise_const hk hl, LinearEquiv.symm_apply_apply]
