mathlib documentation

order.category.PartialOrder

Category of partially ordered types

source
def PartialOrder  :
Type (u_1+1)

The category of partially ordered types.

Equations
source
@[instance]
def PartialOrder.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection partial_order.to_preorder

Equations
source
def PartialOrder.of (α : Type u_1) [partial_order α] :
PartialOrder

Construct a bundled PartialOrder from the underlying type and typeclass.

Equations
source
@[instance]
def PartialOrder.inhabited  :
inhabited PartialOrder

Equations
source
@[instance]
def PartialOrder.partial_order (α : PartialOrder) :
partial_order ↥α

Equations