# mathlib3documentation

order.category.LinOrd

# Category of linear orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def LinOrd  :
Type (u_1+1)

The category of linear orders.

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

Construct a bundled LinOrd from the underlying type and typeclass.

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

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

Equations
@[simp]
theorem LinOrd.dual_map (X Y : LinOrd) (ᾰ : X →o Y) :
@[simp]
def LinOrd.dual  :

order_dual as a functor.

Equations
@[simp]

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

Equations
@[simp]