curryFinFinset_symm_apply_piecewise_const

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

Похожие утверждения