Theorems · Definition · category theory

BddOrd.ofHom

{X Y : Type u} →
  [inst : PartialOrder X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : PartialOrder Y] → [inst_3 : BoundedOrder Y] → BoundedOrderHom X Y → (BddOrd.of X ⟶ BddOrd.of Y)

Typecheck a BoundedOrderHom as a morphism in BddOrd.

Defined in

Mathlib.Order.Category.BddOrd

Cited by

8 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

PartialOrderBoundedOrderPartialOrderBoundedOrder