Theorem WellFounded.not_rel_apply_succ

Modification history

2026-09-11 10:13
Mathlib/Order/WellFounded.lean
refactor: replace `IsWellFounded` with `WellFounded` (#42351) …
Modified WellFounded.not_rel_apply_succView on Github →
2025-01-24 20:24
Mathlib/Order/WellFounded.lean
feat(Order/WellFounded): a relation is well-founded iff there's no infinite decreasing sequence (#21010)
Added WellFounded.not_rel_apply_succView on Github →