Commit 2025-01-24 20:24 6d3806f2

View on Github →

feat(Order/WellFounded): a relation is well-founded iff there's no infinite decreasing sequence (#21010)

Estimated changes

Modified Mathlib/Order/OrderIsoNat.lean

Modified Mathlib/Order/WellFounded.lean

added theorem WellFounded.not_rel_apply_succ

added theorem WellFounded.wellFounded_iff_no_descending_seq