curryEquiv — Mathlib

English

There is a canonical equivalence between n-ary functions (Fin n → α) → β and functions of arity n, i.e., OfArity α β n.

Русский

Существует каноническое эквивалентность между n-арными функциями и функциями арности n, то есть между ((Fin n → α) → β) и Function.OfArity α β n.

LaTeX

$$$\text{curryEquiv}(n) : ((\mathrm{Fin}\ n \to \alpha) \to \beta) \simeq \mathrm{Function.OfArity}\; \alpha\; \beta\; n$$$

Lean4

/-- `Equiv.curry` for n-ary functions. -/
@[simps!]
def curryEquiv (n : ℕ) : ((Fin n → α) → β) ≃ OfArity α β n :=
  FromTypes.curryEquiv _

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