mathlib documentation


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.

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.

def {α β : NonemptyFinLinOrd} (e : α ≃o β) :
α β

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


order_dual as a functor.