mathlib documentation

order.category.PartialOrder

Category of partially ordered types #

def PartialOrder  :
Type (u_1+1)

The category of partially ordered types.

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

Construct a bundled PartialOrder from the underlying type and typeclass.

Equations
@[instance]
Equations