Theorems · Definition · category theory

Preord.ofHom

{X Y : Type u} →
  [inst : Preorder X] →
    [inst_1 : Preorder Y] → (X →o Y) → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })

Typecheck a OrderHom as a morphism in Preord.

Defined in

Mathlib.Order.Category.Preord

Cited by

9 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

PreorderPreorder