English
There is a canonical equivalence between functions of two arguments and the same function with its arguments swapped: (α → β → γ α β) ≃ (β → α → γ α β).
Русский
Существует каноническая эквивалентность между функциями двух аргументов и функциями с переставленными аргументами.
LaTeX
$$$$(\, (\alpha \to \beta \to \gamma(\alpha,\beta)) \,) \cong (\beta \to \alpha \to \gamma(\alpha,\beta)).$$$$
Lean4
/-- `Function.swap` as an equivalence. -/
@[simps (attr := grind =) -fullyApplied]
def functionSwap (α β : Sort*) (γ : α → β → Sort*) : ((a : α) → (b : β) → γ a b) ≃ ((b : β) → (a : α) → γ a b)
where
toFun := Function.swap
invFun := Function.swap
