uncurry_curryLeft — Mathlib

English

The uncurryLeft operation of a continuous linear map followed by curryLeft recovers the original multilinear map.

Русский

Операции uncurryLeft затем curryLeft возвращают исходное многолинейное отображение.

LaTeX

$$$f.uncurryLeft.curryLeft = f$$$

Lean4

@[simp]
theorem uncurry_curryLeft (f : ContinuousMultilinearMap 𝕜 Ei G) : f.curryLeft.uncurryLeft = f :=
  ContinuousMultilinearMap.toMultilinearMap_injective <| f.toMultilinearMap.uncurry_curryLeft

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