mathlib documentation

order.category.LinearOrder

Category of linearly ordered types #

def LinearOrder  :
Type (u_1+1)

The category of linearly ordered types.

Equations
def LinearOrder.of (α : Type u_1) [linear_order α] :

Construct a bundled LinearOrder from the underlying type and typeclass.

Equations
@[instance]
Equations