mathlib documentation

order.​category.​NonemptyFinLinOrd

order.​category.​NonemptyFinLinOrd

# Nonempty finite linear orders

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

@[instance]

@[class]
structure nonempty_fin_lin_ord  :
Type u_1Type u_1

A typeclass for nonempty finite linear orders.

Instances
@[instance]

@[instance]

@[instance]

Equations
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