Better-quasi-ordering (source code)

= Better-quasi-ordering
{wiki}

= Better-quasi-order
{synonym}

= BQO
{c}
{synonym}

A quasi-order is better-quasi-ordered if every array into it from every <barrier in better-quasi-order theory> is good: some barrier members $s\triangleleft t$ satisfy $f(s)\le f(t)$. Singleton barriers recover the usual infinite-sequence condition for a <well-quasi-ordering>. The stronger condition is useful for infinitary closure operations for which well-quasi-ordering alone fails. Equivalently one may use continuous maps from infinite subsets of an infinite subset of the natural numbers, with the discrete topology on the range, and compare $X$ with $X\setminus\{\min X\}$.