English
For curryFinFinset with given cardinalities hk hl, a bilinear map f together with finite index lists mk, ml gives a representation of the curryed map in terms of a single argument built from mk, ml via the finSumEquiv. In particular, curryFinFinset 𝕜 G G' hk hl f mk ml equals the map sending i to f applied to the combination Sum.elim mk ml (finSumEquivOfFinset hk hl).symm i.
Русский
Для curryFinFinset с заданными hk hl, билинейная карта f и конечные списки индексов mk, ml задают представление карри-образной карты через один аргумент, полученный через mk, ml с помощью финального эквивалента Sum. В частности, curryFinFinset hk hl f mk ml равно отображению i в f, применяющуюся к комбинации Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i).
LaTeX
$$$curryFinFinset\\,\\mathstrut 𝕜\\, G\\, G'\\, hk\\ hl\\, f\\, mk\\, ml = f\\Big(\\lambda i,\\;\\text{Sum.elim mk ml}((\\text{finSumEquivOfFinset }hk hl)^{-1} i)\\Big).$$$
Lean4
@[simp]
theorem curryFinFinset_apply (hk : #s = k) (hl : #sᶜ = l) (f : G [×n]→L[𝕜] G') (mk : Fin k → G) (ml : Fin l → G) :
curryFinFinset 𝕜 G G' hk hl f mk ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i) :=
rfl
