continuousMultilinearCurryRightEquiv_apply'

English

In the simplified setting, the application of the primed curryRight equivalence yields the evaluation on the extended input: continuousMultilinearCurryRightEquiv' 𝕜 n G G' f v x = f (snoc v x).

Русский

В упрощённом виде применение primed curryRight эквивалентности даёт значение на расширенном аргументе: continuousMultilinearCurryRightEquiv' 𝕜 n G G' f v x = f (snoc v x).

LaTeX

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

Lean4

@[simp]
theorem continuousMultilinearCurryRightEquiv_apply' (f : G [×n.succ]→L[𝕜] G') (v : Fin n → G) (x : G) :
    continuousMultilinearCurryRightEquiv' 𝕜 n G G' f v x = f (snoc v x) :=
  rfl

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