Theorem exists_not_acc_lt_of_not_acc

Modification history

2025-08-15 22:00

Mathlib/Order/WellFounded.lean

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

Added exists_not_acc_lt_of_not_acc View on Github →