Commit 2025-02-13 21:54 44f77fa1

View on Github →

feat(Order/WellQuasiOrder): WellQuasiOrdered predicate (#21008) We define the WellQuasiOrdered predicate for an unbundled WQO relation, and the WellQuasiOrderedLE typeclass. We show some basic properties of them both. Note that we already have the set versions Set.PartiallyWellOrderedOn and Set.IsPWO. A future PR will redefine the set predicates in terms of the type predicates. We call these WQOs instead of PWOs, since we're not actually requiring a partial order, but only a quasiorder (preorder).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/WellQuasiOrder.lean

added theorem Finite.wellQuasiOrdered

added theorem IsAntichain.finite_of_wellQuasiOrdered

added theorem WellQuasiOrdered.exists_monotone_subseq

added theorem WellQuasiOrdered.prod

added theorem WellQuasiOrdered.wellFounded

added def WellQuasiOrdered

added theorem WellQuasiOrderedLE.finite_of_isAntichain

added theorem wellQuasiOrderedLE_iff

added theorem wellQuasiOrderedLE_iff_wellFoundedLT

added theorem wellQuasiOrdered_iff_exists_monotone_subseq

added theorem wellQuasiOrdered_le

added theorem wellQuasiOrdered_of_isEmpty