mathlib documentation

order.category.LinearOrder

Category of linearly ordered types

source
def LinearOrder  :
Type (u_1+1)

The category of linearly ordered types.

Equations
source
@[instance]
def LinearOrder.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection linear_order.to_partial_order

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

Construct a bundled LinearOrder from the underlying type and typeclass.

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

Equations
source
@[instance]
def LinearOrder.linear_order (α : LinearOrder) :
linear_order ↥α

Equations