Theorem acc_iff_isEmpty_descending_chain

Modification history

2025-08-15 22:00

Mathlib/Order/WellFounded.lean

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

Added acc_iff_isEmpty_descending_chain View on Github →