currySum_apply — Mathlib

English

For f, currySum f evaluated at u and v yields f evaluated at the combined input obtained by merging u and v via Sum.rec.

Русский

Для f, currySum f при заданных u и v даёт значение f в аргументе, полученном объединением u и v через Sum.rec.

LaTeX

$$$\\text{currySum}(f)(u)(v) = f(\\mathrm{SumRec}(u,v))$$$

Lean4

@[simp low]
theorem currySum_apply (f : MultilinearMap R N M₂) (u : (i : ι) → N (Sum.inl i)) (v : (i : ι') → N (Sum.inr i)) :
    currySum f u v = f (Sum.rec u v) :=
  rfl

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