continuousMultilinearCurryLeftEquiv_symm_apply

English

Applying curryLeft to f at a use-case yields the expected concatenation with cons.

Русский

Применение curryLeft к f в конкретном случае даёт ожидаемое сцепление с конструкцией-константой.

LaTeX

$$$f.curryLeft\ x\; m = f(\text{cons } x\; m)$$$

Lean4

@[simp]
theorem continuousMultilinearCurryLeftEquiv_symm_apply
    (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei i.succ) G) (v : Π i, Ei i) :
    (continuousMultilinearCurryLeftEquiv 𝕜 Ei G).symm f v = f (v 0) (tail v) :=
  rfl

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