Rado order (source code)

= Rado order
{c}
{title2=$R$}

The Rado order has domain $R=\{(m,n)\in\mathbb N^2:m<n\}$ and $(m,n)\le_R(k,l)$ iff either $m=k$ and $n\le l$, or $n<k$. It is a <well-quasi-ordering>: either one row recurs infinitely in a <sequence>, or the first coordinates are unbounded and yield a cross-row comparison. Its infinite rows form an infinite <antichain> under <Hoare domination preorder>, showing that arbitrary-subset lifting need not preserve <well-quasi-ordering>.