uncurry_curryRight — Mathlib

English

Let f be a continuous multilinear map with indexed arguments; applying curryRight and then uncurryRight returns the original map: f = (f.curryRight).uncurryRight.

Русский

Пусть f — непрерывная многодлинейная отображения; применение curryRight, затем uncurryRight возвращает исходное отображение: f = (f.curryRight).uncurryRight.

LaTeX

$$$f.curryRight.uncurryRight = f$$$

Lean4

@[simp]
theorem uncurry_curryRight (f : ContinuousMultilinearMap 𝕜 Ei G) : f.curryRight.uncurryRight = f :=
  by
  ext m
  rw [uncurryRight_apply, curryRight_apply, snoc_init_self]

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