Theorem WellFounded.not_rel_apply_succ

Modification history

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 →