English
There is an order isomorphism between order homomorphisms α → β and the dual of order homomorphisms (OrderDual α) → (OrderDual β).
Русский
Существует упорядоченный изоморфизм между отображениями порядка α → β и дуализацией отображений порядка (OrderDual α) → (OrderDual β).
LaTeX
$$$\\operatorname{dualIso}_{\\alpha,\\beta} : (\\alpha \\to_o \\beta) \\cong_o \\big( \\mathrm{OrderDual}( \\mathrm{OrderHom}( \\mathrm{OrderDual}\\alpha)(\\mathrm{OrderDual}\\beta) ) \\big).$$$
Lean4
/-- `OrderHom.dual` as an order isomorphism. -/
def dualIso (α β : Type*) [Preorder α] [Preorder β] : (α →o β) ≃o (αᵒᵈ →o βᵒᵈ)ᵒᵈ
where
toEquiv := OrderHom.dual.trans OrderDual.toDual
map_rel_iff' := Iff.rfl
