Theorem wellFoundedGT_iff_monotone_chain_condition'

Modification history

2025-02-08 23:59
Mathlib/Order/OrderIsoNat.lean
refactor(Order/OrderIsoNat): use `WellFoundedGT` in monotone chain condition (#20782) …
Added wellFoundedGT_iff_monotone_chain_condition'View on Github →