# mathlib3documentation

order.category.Preord

# Category of preorders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines Preord, the category of preorders with monotone maps.

def Preord  :
Type (u_1+1)

The category of preorders.

Equations
Instances for Preord
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
def Preord.of (α : Type u_1) [preorder α] :

Construct a bundled Preord from the underlying type and typeclass.

Equations
@[simp]
theorem Preord.coe_of (α : Type u_1) [preorder α] :
(Preord.of α) = α
@[protected, instance]
Equations
@[protected, instance]
def Preord.preorder (α : Preord) :
Equations
@[simp]
theorem Preord.iso.mk_hom {α β : Preord} (e : α ≃o β) :
@[simp]
theorem Preord.iso.mk_inv {α β : Preord} (e : α ≃o β) :
def Preord.iso.mk {α β : Preord} (e : α ≃o β) :
α β

Constructs an equivalence between preorders from an order isomorphism between them.

Equations
@[simp]
def Preord.dual  :

order_dual as a functor.

Equations
@[simp]
theorem Preord.dual_map (X Y : Preord) (ᾰ : X →o Y) :
@[simp]
@[simp]

The equivalence between Preord and itself induced by order_dual both ways.

Equations

The embedding of Preord into Cat.

Equations
Instances for Preord_to_Cat
@[simp]
theorem Preord_to_Cat_map (X Y : Preord) (f : X Y) :
@[simp]
theorem Preord_to_Cat_obj (X : Preord) :
@[protected, instance]
@[protected, instance]
Equations