English
There is a natural equivalence between monotone maps α → β and monotone maps αᵒᵈ → βᵒᵈ; i.e., the dual construction yields an order isomorphism between these sets of maps.
Русский
Существует естественное эквивалентное соответствие между монотонными отображениями α → β и αᵒᵈ → βᵒᵈ; дуальная конструкция задаёт упорядоченное изоморфизм между множествами таких отображений.
LaTeX
$$$(\\alpha \\to_o \\beta) \\cong_o (\\alpha^{\\mathrm{op}} \\to_o \\beta^{\\mathrm{op}})$.$$
Lean4
/-- Reinterpret a bundled monotone function as a monotone function between dual orders. -/
@[simps]
protected def dual : (α →o β) ≃ (αᵒᵈ →o βᵒᵈ)
where
toFun f := ⟨(OrderDual.toDual : β → βᵒᵈ) ∘ (f : α → β) ∘ (OrderDual.ofDual : αᵒᵈ → α), f.mono.dual⟩
invFun f := ⟨OrderDual.ofDual ∘ f ∘ OrderDual.toDual, f.mono.dual⟩
