Theorem not_acc_iff_exists_descending_chain

Modification history

2025-08-15 22:00

Mathlib/Order/WellFounded.lean

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

Added not_acc_iff_exists_descending_chain View on Github →