mathlib documentation

order.category.Preorder

Category of preorders #

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

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

Construct a bundled Preorder from the underlying type and typeclass.

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

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

Equations
@[simp]
theorem Preorder.iso.mk_inv {α β : Preorder} (e : α ≃o β) :
@[simp]
theorem Preorder.iso.mk_hom {α β : Preorder} (e : α ≃o β) :

order_dual as a functor.

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

The embedding of Preorder into Cat.

Equations
Instances for Preorder_to_Cat
@[simp]
theorem Preorder_to_Cat_map (X Y : Preorder) (f : X Y) :
@[protected, instance]
Equations