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_1) :
Type 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