mathlib documentation

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.

@[class]
structure nonempty_fin_lin_ord (α : Type u_1) :
Type u_1

A typeclass for nonempty finite linear orders.

Instances of this typeclass
Instances of other typeclasses for nonempty_fin_lin_ord
  • nonempty_fin_lin_ord.has_sizeof_inst

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations
@[simp]
def NonemptyFinLinOrd.iso.mk {α β : NonemptyFinLinOrd} (e : α ≃o β) :
α β

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

Equations

order_dual as a functor.

Equations