Theorems · Definition · order theory

OrderHom.toFunctor

{X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → (X →o Y) → CategoryTheory.Functor X Y

An OrderHom as a functor X ⥤ Y between preorder categories.

Defined in

Mathlib.CategoryTheory.Category.Preorder

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

PreorderPreorder