curryMid_uncurryMid — Mathlib

English

CurryMid and uncurryMid are inverses: applying curryMid and then uncurryMid returns the original map.

Русский

CurryMid и uncurryMid образуют пары-обратные: применение curryMid, далее uncurryMid возвращает исходное отображение.

LaTeX

$$$(f.curryMid p).uncurryMid p = f$$$

Lean4

@[simp]
theorem curryMid_uncurryMid (p : Fin (n + 1))
    (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i ↦ Ei (p.succAbove i)) G) : (f.uncurryMid p).curryMid p = f := by
  ext; simp

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