continuousMultilinearCurryRightEquiv_symm_apply

English

The symmetric curryRight equivalence acts so that, for a suitable f and v, the inverse map yields f evaluated at the initial segment and the last component: (continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f v = f (init v) (v (last n)).

Русский

Симметричная эквивалентность curryRight даёт, что: (continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f v = f (init v) (v (last n)).

LaTeX

$$$\\,(continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f\,v = f(\\mathrm{init}\\,v)\, (v(\\mathrm{last}\\,n))$$$

Lean4

@[simp]
theorem continuousMultilinearCurryRightEquiv_symm_apply
    (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G)) (v : Π i, Ei i) :
    (continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f v = f (init v) (v (last n)) :=
  rfl

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