curryLeft_apply_apply — Mathlib

English

For a curryLeft map, applying it in x and then evaluating on v yields the same as evaluating the original map on the concatenated vector (x :: v).

Русский

Применяя curryLeft к переменной x и затем вычисляя на v, получаем значение исходного отображения на векторе, полученном объединением x и v.

LaTeX

$$$(f.curryLeft x) v = f (Matrix.vecCons x v)$$$

Lean4

@[simp]
theorem curryLeft_apply_apply (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) (v : Fin n → E) :
    curryLeft f x v = f (Matrix.vecCons x v) :=
  rfl

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