# Documentation

Mathlib.Order.Category.NonemptyFinLinOrd

# 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
Equations
Equations
• = NonemptyFiniteLinearOrder.mk
Equations
Equations
• = let src := ; NonemptyFiniteLinearOrder.mk
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
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_hom {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
.hom = e
@[simp]
theorem NonemptyFinLinOrd.Iso.mk_inv {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
.inv = ()
def NonemptyFinLinOrd.Iso.mk {α : NonemptyFinLinOrd} {β : NonemptyFinLinOrd} (e : α ≃o β) :
α β

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

Equations
Instances For
@[simp]
theorem NonemptyFinLinOrd.dual_map :
∀ {X Y : NonemptyFinLinOrd} (a : X →o Y), = OrderHom.dual a

OrderDual as a functor.

Equations
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
• One or more equations did not get rendered due to their size.

The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd and order_dual commute.

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