English
The symmetric curryFinFinset commutes with piecewise-constant inputs: applying symm to a map f and a piecewise-constant function s.piecewise(constant x, constant y) yields the constant combination f(const x) and f(const y).
Русский
Симметричное каррирование сохраняет разбиение по участкам: применение symm к f и кусочно-постоянной функции даёт те же константные аргументы.
LaTeX
$$$((curryFinFinset\\, 𝕜\\ G\\ G' hk hl).symm\\ f)\\ (s\\.piecewise(\\lambda\\_ => x) (\\lambda\\_ => y)) = f(\\lambda\\_ => x)\\ (\\lambda\\_ => y).$$$
Lean4
theorem curryFinFinset_symm_apply_piecewise_const (hk : #s = k) (hl : #sᶜ = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G')
(x y : G) :
(curryFinFinset 𝕜 G G' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) = f (fun _ => x) fun _ => y :=
MultilinearMap.curryFinFinset_symm_apply_piecewise_const hk hl _ x y