uncurry_curry — Mathlib

English

There is a standard theorem that uncurry and curry are mutual inverses, i.e., curry (uncurry f) = f and uncurry (curry f) = f.

Русский

Существуют две взаимно обратные операции: uncurry и curry, причём curry (uncurry f) = f и uncurry (curry f) = f.

LaTeX

$$$\\text{curry }(\\text{uncurry } f) = f$ and $\\text{uncurry }(\\text{curry } f) = f$$$

Lean4

@[simp]
theorem uncurry_curry (f : ((i : Fin n) → p i) → τ) : uncurry (curry f) = f :=
  by
  ext args
  induction n with
  | zero => exact congrArg f (Subsingleton.allEq _ _)
  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

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