Ordinal rank function for a relation (source code)

= Ordinal rank function for a relation
{title2=$\rho:X\to\operatorname{Ord}$}

An ordinal-valued function strictly increasing along a relation. For a well-founded set relation, or a <set-like> class relation, the canonical rank is $\rho(y)=\sup\{\rho(x)+1:xRy\}$.