Commit 2025-10-23 14:48 69098f8e

View on Github →

feat(Order/WellFoundedSet): partiallyWellOrderedOn_univ_iff and Pi.wellQuasiOrderedLE (#30275) Connect Set.PartiallyWellOrderedOn with WellQuasiOrdered and Set.IsPWO with WellQuasiOrderedLE. Add an instance Pi.wellQuasiOrderedLE for Dickson's lemma.

Estimated changes

Modified Mathlib/Order/RelIso/Set.lean

added def RelIso.subrelUnivIso

Modified Mathlib/Order/WellFoundedSet.lean

added theorem Set.isPWO_of_wellQuasiOrderedLE

added theorem Set.isPWO_univ_iff

added theorem Set.partiallyWellOrderedOn_of_wellQuasiOrdered

added theorem Set.partiallyWellOrderedOn_univ_iff

Modified Mathlib/Order/WellQuasiOrder.lean

added theorem RelIso.wellQuasiOrdered_iff