# Nonempty finite linear orders #

This defines NonemptyFinLinOrd, the category of nonempty finite linear orders with monotone maps. This is the index category for simplicial objects.

Note: NonemptyFinLinOrd is not a subcategory of FinBddDistLat because its morphisms do not preserve ⊥ and ⊤.

class NonemptyFiniteLinearOrder (α : Type u_1) extends , :
Type u_1

A typeclass for nonempty finite linear orders.

• elems :
• complete : ∀ (x : α), x Fintype.elems
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun (x x_1 : α) => x x_1
• decidableEq :
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• Nonempty :
Instances
theorem NonemptyFiniteLinearOrder.Nonempty {α : Type u_1} [self : ] :
@[instance 100]
Equations
Equations
Equations
• = let __src := ;
def NonemptyFinLinOrd :
Type (u_1 + 1)

The category of nonempty finite linear orders.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations
Instances For
@[simp]
theorem NonemptyFinLinOrd.coe_of (α : Type u_1) :
= α
Equations
• α.instNonemptyFiniteLinearOrderα = α.str
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem NonemptyFinLinOrd.Iso.mk_inv {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
.inv = e.symm
@[simp]
theorem NonemptyFinLinOrd.Iso.mk_hom {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
.hom = e
def NonemptyFinLinOrd.Iso.mk {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
α β

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

Equations
• = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem NonemptyFinLinOrd.dual_map :
∀ {X Y : NonemptyFinLinOrd} (a : X →o Y), = OrderHom.dual a

OrderDual as a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]

The equivalence between NonemptyFinLinOrd and itself induced by OrderDual both ways.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• NonemptyFinLinOrd.instFunLikeHomαNonemptyFiniteLinearOrder = { coe := fun (f : A B) => (let_fun this := f; this), coe_injective' := }
theorem NonemptyFinLinOrd.forget_map_apply {A : NonemptyFinLinOrd} {B : NonemptyFinLinOrd} (f : A B) (a : A) :
= f.toFun a

The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd and OrderDual commute.

Equations
• One or more equations did not get rendered due to their size.
Instances For