curryMid_uncurryMid — Mathlib

English

The operation curryMid followed by uncurryMid returns the original linear map: (f.uncurryMid i).curryMid i = f.

Русский

Операция curryMid затем uncurryMid восстанавливает изначальное линейное отображение: (f.uncurryMid i).curryMid i = f.

LaTeX

$$$ (f.\\text{uncurryMid}\, i).\\text{curryMid}\, i = f $$$

Lean4

@[simp]
theorem curryMid_uncurryMid (i : Fin (n + 1)) (f : M i →ₗ[R] MultilinearMap R (fun j ↦ M (i.succAbove j)) M₂) :
    (f.uncurryMid i).curryMid i = f := by ext; simp

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