English
For the symmetric curryFinFinset, applying the inverse (symm) to a bilinear map f and a function m : Fin n → G yields the two-argument application of f to the left and right components obtained by composing m with the standard finSumEquiv. Concretely, (curryFinFinset hk hl).symm f m = f (m ∘ finSumEquivOfFinset hk hl).inl) (m ∘ finSumEquivOfFinset hk hl).inr).
Русский
Для симметричной каррифинсетной операции принимает форму равенства: (curryFinFinset hk hl).symm f m = f (множество слева) (множество справа), полученных через конституенты m и финального эквивалента.
LaTeX
$$$\\big(\\,\\text{curryFinFinset }\\ 𝕜\\ G\\ G'\\ hk\\ hl\\big).\\text{symm }f\\;m = f\\Big(\\lambda i, m\\Bigl(\\mathrm{finSumEquivOfFinset } hk hl \\mathrm{.inl } i\\Bigr)\\Big)\\;\\lambda i, m\\Bigl(\\mathrm{finSumEquivOfFinset } hk hl \\mathrm{.inr } i\\Bigr)\\Big).$$$
Lean4
@[simp]
theorem curryFinFinset_symm_apply (hk : #s = k) (hl : #sᶜ = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G') (m : Fin n → G) :
(curryFinFinset 𝕜 G G' hk hl).symm f m =
f (fun i => m <| finSumEquivOfFinset hk hl (Sum.inl i)) fun i => m <| finSumEquivOfFinset hk hl (Sum.inr i) :=
rfl
