Reverse-inclusion well-quasi-ordering of monomial ideals (source code)

= Reverse-inclusion well-quasi-ordering of monomial ideals

= Maclagan's theorem
{c}
{synonym}

Upward-closed subsets of $\mathbb N^r$, including the empty subset, form a <well-quasi-ordering> by reverse inclusion. For $r=1$, tails correspond to the well-order $\mathbb N\cup\{\infty\}$. Inductively slice in the last coordinate. The slices increase and eventually stabilize: their union has a finite minimal basis by the <Dickson lemma>, all of which has appeared in one finite slice. Encode an upset by the word of its pre-stabilization slices and its final slice. The <Higman lemma> and <finite product closure of well-quasi-orderings> compare these encodings in the reverse-inclusion slice order. A subsequence map $f$ has $f(k)\ge k$, so containment of the matched later slice implies containment of the slice at $k$; the final-slice comparison handles the tail. The entire earlier upset therefore contains the later upset.