# mathlibdocumentation

order.category.LinearOrder

# Category of linear orders #

This defines LinearOrder, the category of linear orders with monotone maps.

def LinearOrder  :
Type (u_1+1)

The category of linear orders.

Equations
Instances for LinearOrder
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def LinearOrder.has_coe_to_sort  :
(Type u_1)
Equations
def LinearOrder.of (α : Type u_1) [linear_order α] :

Construct a bundled LinearOrder from the underlying type and typeclass.

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

Constructs an equivalence between linear orders from an order isomorphism between them.

Equations
@[simp]
theorem LinearOrder.iso.mk_inv {α β : LinearOrder} (e : α ≃o β) :
= (e.symm)
@[simp]
theorem LinearOrder.iso.mk_hom {α β : LinearOrder} (e : α ≃o β) :
= e
@[simp]
@[simp]
theorem LinearOrder.dual_map (X Y : LinearOrder) (ᾰ : X →o Y) :

order_dual as a functor.

Equations
@[simp]
@[simp]

The equivalence between LinearOrder and itself induced by order_dual both ways.

Equations