mathlib documentation

order.category.LinearOrder

Category of linear orders #

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

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
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 β) :
@[simp]
theorem LinearOrder.iso.mk_hom {α β : LinearOrder} (e : α ≃o β) :
@[simp]

order_dual as a functor.

Equations