English
Curry/uncurry gives an order isomorphism between OrderHom(Prod α β, γ) and OrderHom α (OrderHom β γ).
Русский
Кёрри/ uncurry задают отображение порядка между OrderHom(Prod α β, γ) и OrderHom α (OrderHom β γ).
LaTeX
$$$\\text{curry} : (α × β →_o γ) \\simeq_o (α →_o β →_o γ)$$$
Lean4
/-- Curry/uncurry as an order isomorphism between `α × β →o γ` and `α →o β →o γ`. -/
def curry : (α × β →o γ) ≃o (α →o β →o γ)
where
toFun f := ⟨fun x ↦ ⟨Function.curry f x, fun _ _ h ↦ f.mono ⟨le_rfl, h⟩⟩, fun _ _ h _ => f.mono ⟨h, le_rfl⟩⟩
invFun f := ⟨Function.uncurry fun x ↦ f x, fun x y h ↦ (f.mono h.1 x.2).trans ((f y.1).mono h.2)⟩
map_rel_iff' := by simp [le_def]
