mathlib documentation

order.category.NonemptyFinLinOrd

# Nonempty finite linear orders

Nonempty finite linear orders form the index category for simplicial objects.

@[instance]

@[instance]

@[instance]

@[instance]
def nonempty_fin_lin_ord.to_fintype (α : Type u_1) [s : nonempty_fin_lin_ord α] :

@[class]
structure nonempty_fin_lin_ord  :
Type u_1Type u_1

A typeclass for nonempty finite linear orders.

Instances
def NonemptyFinLinOrd  :
Type (u_1+1)

The category of nonempty finite linear orders.

Equations

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations