curryFinFinset_apply_const — Mathlib

English

A curryFinFinset with constant arguments reproduces the original map on the piecewise input: curryFinFinset hk hl f (const x) (const y) = f(s.piecewise(const x) const y).

Русский

КарриFinFinset с константами возвращает исходную карту на склеенном входе через piecewise.

LaTeX

$$$\\curryFinFinset\\,\\mathbb{R}\\ G\\ G' hk hl\\ f\\ (\\lambda _ => x)\\ (\\lambda _ => y) = f\\big( s\\.piecewise(\\lambda _ => x) (\\lambda _ => y) \\big).$$$

Lean4

theorem curryFinFinset_apply_const (hk : #s = k) (hl : #sᶜ = l) (f : G [×n]→L[𝕜] G') (x y : G) :
    (curryFinFinset 𝕜 G G' hk hl f (fun _ => x) fun _ => y) = f (s.piecewise (fun _ => x) fun _ => y) :=
  by
  refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_
  rw [LinearIsometryEquiv.symm_apply_apply]

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