English
There is a canonical equivalence between functions of two arguments and curried functions: (α × β → γ) ≃ (α → β → γ).
Русский
Существует каноническое эквивалентность между функциями двух аргументов и каррированными функциями: (α × β → γ) ≃ (α → β → γ).
LaTeX
$$$$ (\\alpha \\times \\beta \\to \\gamma) \\simeq (\\alpha \\to \\beta \\to \\gamma). $$$$
Lean4
/-- `γ`-valued functions on `α × β` are equivalent to functions `α → β → γ`. -/
@[simps (attr := grind =) -fullyApplied]
def curry (α β γ) : (α × β → γ) ≃ (α → β → γ)
where
toFun := Function.curry
invFun := uncurry
left_inv := uncurry_curry
right_inv := curry_uncurry
