Commit 2025-11-24 13:11 fc892cf1
View on Github →feat(Order): reprove Dickson's lemma (#31514)
Reprove Dickson's lemma Pi.wellQuasiOrderedLE under assumption of preorder and well-quasi-order, and generalize it to any relation and/or product of well-quasi-ordered sets. Also add an instance of WellQuasiOrderedLE from LinearOrder and WellFoundedLT.
Pi.isPWO and Finsupp.isPWO are deprecated since they are superseded by isPWO_of_wellQuasiOrderedLE and instances.