curryLeft_apply — Mathlib

English

Curry and uncurryLeft form inverse equivalences between certain linear maps and multilinear maps; applying one after the other returns the original map.

Русский

Операторы curry и uncurryLeft образуют взаимно обратные эквивалентности между линейными и многолинейными отображениями; применение одного после другого возвращает исходное отображение.

LaTeX

$$$f.\text{uncurryLeft}.curryLeft = f$$$

Lean4

@[simp]
theorem curryLeft_apply (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0) (m : ∀ i : Fin n, Ei i.succ) :
    f.curryLeft x m = f (cons x m) :=
  rfl

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