curry_uncurryRight — Mathlib

English

Applying uncurryRight to inputs yields the evaluation at init m and last coordinate.

Русский

Применение uncurryRight даёт значение на init m и последнюю координату.

LaTeX

$$$$f.uncurryRight m = f (init m) (m (last n)).$$$$

Lean4

@[simp]
theorem curry_uncurryRight (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) :
    f.uncurryRight.curryRight = f := by
  ext m x
  simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]
  rw [init_snoc]

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