Commit 2025-03-18 05:03 f7b6fa64

View on Github →

feat: merge wqo APIs (#20786) PR #21008 previously introduced a WellQuasiOrdered predicate and a WellQuasiOrderedLE typeclass. This PR unifies these with the preexisting Set.PartiallyWellOrderedOn and Set.IsPWO predicates. A future PR will rename PartiallyWellOrderedOn to WellQuasiOrderedOn and IsPWO to IsWQO, since these are the more common names.

Estimated changes

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/Data/Set/MulAntidiagonal.lean

Modified Mathlib/Data/Set/SMulAntidiagonal.lean

Modified Mathlib/Order/WellFoundedSet.lean

modified theorem Set.IsPWO.of_linearOrder

modified theorem Set.IsWF.of_wellFoundedLT

added theorem Set.PartiallyWellOrderedOn.exists_lt

modified theorem Set.PartiallyWellOrderedOn.exists_monotone_subseq

modified theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂

modified theorem Set.PartiallyWellOrderedOn.wellFoundedOn

modified theorem Set.isPWO_iff_isWF

modified theorem Set.isWF_univ_iff

modified theorem Set.partiallyWellOrderedOn_empty

added theorem Set.partiallyWellOrderedOn_iff_exists_lt

modified theorem WellFounded.isWF

Modified Mathlib/Order/WellQuasiOrder.lean

Modified Mathlib/RingTheory/HahnSeries/PowerSeries.lean