strict-order

Parent: basic-orders

Strict (partial) order

A relation < that is irreflexive (a < a never holds) and transitive. (Irreflexive + transitive already implies asymmetry.)

It's the < shadow of a ≤: from a partial-order ≤, set a < b ⟺ a≤b ∧ a≠b; conversely a ≤ b ⟺ a<b ∨ a=b. The two forms carry the same information.

A strict total order additionally has trichotomy: for all a,b exactly one of a<b, a=b, b<a holds. Strict orders are the natural setting for well-foundedness ("no infinite … < a₂ < a₁") and hence for ordinals and well-founded recursion.