Commit 2025-08-15 22:00 02207698

View on Github →

feat(Order/WellFounded): Acc and infinite descending chain (#28120)

Estimated changes

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/CategoryTheory/Subobject/ArtinianObject.lean

Modified Mathlib/CategoryTheory/Subobject/NoetherianObject.lean

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/Height.lean

Modified Mathlib/Order/OrderIsoNat.lean

added theorem RelEmbedding.acc_iff_isEmpty_subtype_mem_range

deleted theorem RelEmbedding.acc_iff_no_decreasing_seq

deleted theorem RelEmbedding.exists_not_acc_lt_of_not_acc

added theorem RelEmbedding.not_acc

deleted theorem RelEmbedding.not_acc_of_decreasing_seq

added theorem RelEmbedding.not_wellFounded

deleted theorem RelEmbedding.not_wellFounded_of_decreasing_seq

added theorem RelEmbedding.wellFounded_iff_isEmpty

deleted theorem RelEmbedding.wellFounded_iff_no_descending_seq

Modified Mathlib/Order/RelSeries.lean

Modified Mathlib/Order/WellFounded.lean

deleted theorem WellFounded.wellFounded_iff_no_descending_seq

added theorem acc_def

added theorem acc_iff_isEmpty_descending_chain

added theorem exists_not_acc_lt_of_not_acc

added theorem not_acc_iff_exists_descending_chain

added theorem wellFounded_iff_isEmpty_descending_chain

Modified Mathlib/Order/WellFoundedSet.lean

Modified Mathlib/Order/WellQuasiOrder.lean

Modified Mathlib/RingTheory/Artinian/Module.lean