Finite product closure of well-quasi-orderings
ID: finite-product-closure-of-well-quasi-orderings
A finite Cartesian product of well-quasi-orderings is well-quasi-ordered in the componentwise order. Every infinite sequence in one well-quasi-order has an infinite nondecreasing subsequence: colour pairs by whether they are ordered, apply Ramsey's theorem, and exclude an all-bad subsequence. Restrict successively to such a subsequence in each coordinate. The same argument, or the infinite pigeonhole principle, proves closure under finite disjoint unions with no cross-component comparisons.
New to topics? Read the docs here!