Strict total order (source code)

= Strict total order

A strict total order is an irreflexive and transitive relation $<$ for which exactly one of $x<y$ and $y<x$ holds whenever $x\ne y$. It corresponds to a total order through $x\leq y$ if and only if $x<y$ or $x=y$.