curry_two_eq_curry — Mathlib

English

For two-argument functions, curry can be expressed via a precomposition with the standard two-argument rearrangement; i.e., curry f equals the curry of f composed with the inverse of the two-argument bijection.

Русский

Для двухарной функции карри может быть выражено через предсвязку с каноническим переупорядочиванием; то есть curry f = curry (f ∘ (finTwoArrowEquiv α).symm).

LaTeX

$$$\forall f: ((i:\mathrm{Fin}\ 2) \to \alpha) \to \beta,\quad \operatorname{curry} f = \operatorname{Function.curry}(f \circ (\mathrm{finTwoArrowEquiv}\ \alpha)^{-1})$$$

Lean4

theorem curry_two_eq_curry {α β : Type u} (f : ((i : Fin 2) → α) → β) :
    curry f = Function.curry (f ∘ (finTwoArrowEquiv α).symm) :=
  FromTypes.curry_two_eq_curry f

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