Theorems · Definition · order theory

BoundedOrderHom.dual

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : BoundedOrder α] →
        [inst_2 : Preorder β] → [inst_3 : BoundedOrder β] → BoundedOrderHom α β ≃ BoundedOrderHom αᵒᵈ βᵒᵈ

Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.

Defined in

Mathlib.Order.Hom.Bounded

Cited by

7 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

PreorderBoundedOrderPreorderBoundedOrder