Linear orders as rankings

This entry formalises the obvious isomorphism between finite linear orders and lists, where the list in question is interpreted as a ranking, i.e. it lists the elements in descending order without repetition.

It also provides an executable algorithm to compute topological sortings, i.e. all rankings whose linear orders are extensions of a given relation.