Theorem not_strictMono_of_wellFoundedGT

Modification history

2025-01-19 21:48

Mathlib/Order/OrderIsoNat.lean

feat(Order/OrderIsoNat): sequence in well-founded order is not `StrictAnti` (#20851)

Added not_strictMono_of_wellFoundedGT View on Github →