English
There is a natural equivalence between bounded order homomorphisms α→β and αᵒᵈ→βᵒᵈ, given by taking duals.
Русский
Существует естественное эквиваленство между гомоморфизмами ограниченного порядка от α к β и от αᵒᵈ к βᵒᵈ, задаваемое двойственной операцией.
LaTeX
$$$\mathrm{BoundedOrderHom.dual} : \mathrm{BoundedOrderHom}(\alpha,\beta) \simeq \mathrm{BoundedOrderHom}(\alpha^{\mathrm{op}}, \beta^{\mathrm{op}})$$$
Lean4
/-- Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual
orders. -/
@[simps]
protected def dual : BoundedOrderHom α β ≃ BoundedOrderHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨f.toOrderHom.dual, f.map_bot', f.map_top'⟩
invFun f := ⟨OrderHom.dual.symm f.toOrderHom, f.map_bot', f.map_top'⟩
