continuousMultilinearCurryRightEquiv_symm_apply'

English

The symmetric primed curryRight equivalence acts so that its inverse applied to f and v equals f applied to the initial segment and the last coordinate: (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 : G [×n]→L[𝕜] G →L[𝕜] G') (v : Fin (n + 1) → G) :
    (continuousMultilinearCurryRightEquiv' 𝕜 n G G').symm f v = f (init v) (v (last n)) :=
  rfl

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