curryLeft — Mathlib

English

Applying uncurryLeft to a fixed m yields the evaluation with m0 and tail m.

Русский

Применение uncurryLeft к фиксированному m даёт оценку на m0 и хвост m.

LaTeX

$$$$f.uncurryLeft m = f (m 0) (tail m).$$$$

Lean4

/-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
a linear map into multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`. -/
def curryLeft (f : MultilinearMap R M M₂) : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂
    where
  toFun x := MultilinearMap.mk' fun m => f (cons x m)
  map_add' x
    y := by
    ext m
    exact cons_add f m x y
  map_smul' c
    x := by
    ext m
    exact cons_smul f m c x

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