continuousMultilinearCurryRightEquiv_apply

English

For f and inputs v, x, the curryRight equivalence evaluated at v and x equals f on the extended input snoc v x: (continuousMultilinearCurryRightEquiv 𝕜 Ei G f) v x = f (snoc v x).

Русский

Пусть f и входы v, x; оценка эквивалентности curryRight даёт равенство: (continuousMultilinearCurryRightEquiv 𝕜 Ei G f) v x = f (snoc v x).

LaTeX

$$$\\,(continuousMultilinearCurryRightEquiv 𝕜 Ei G f)\\,v\\,x = f(\\mathrm{snoc}\\,v\\,x)\\,$$$

Lean4

@[simp]
theorem continuousMultilinearCurryRightEquiv_apply (f : ContinuousMultilinearMap 𝕜 Ei G)
    (v : Π i : Fin n, Ei <| castSucc i) (x : Ei (last n)) :
    continuousMultilinearCurryRightEquiv 𝕜 Ei G f v x = f (snoc v x) :=
  rfl

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