curry_uncurry — Mathlib

English

Alternatively, curry and uncurry form an equivalence between functions on tuples and FromTypes p τ.

Русский

Альтернативно, каррирование и раскаррирование образуют эквиваленцию между функциями на кортежах и FromTypes p τ.

LaTeX

$$$\\text{curryEquiv}(p,\\tau) : (((i:\\mathrm Fin n)→ p i)→τ) \\simeq \\mathrm{FromTypes}\; p\\tau$$$

Lean4

@[simp]
theorem curry_uncurry (f : Function.FromTypes p τ) : curry (uncurry f) = f := by
  induction n with
  | zero => rfl
  | succ n ih => exact funext (ih <| f ·)

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