uncurrySum_currySum — Mathlib

English

Applying uncurrySum to g yields its evaluation on the arguments split into the left and right parts.

Русский

Применение uncurrySum к g даёт значение отображения на разложении по левой и правой частям.

LaTeX

$$$\\text{uncurrySum}(g)(u) = g(\\lambda i. u(\\mathrm{inl}\, i))(\\lambda i'. u(\\mathrm{inr}\, i'))$$$

Lean4

@[simp]
theorem uncurrySum_currySum (f : MultilinearMap R N M₂) : uncurrySum (currySum f) = f :=
  by
  ext
  simp only [uncurrySum_apply, currySum_apply]
  congr
  ext (_ | _) <;> simp

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