Theorem Infinite.exists_strictMono_or_strictAnti

Modification history

2026-07-13 17:10
Mathlib/Order/OrderIsoNat.lean
feat(Order/OrderIsoNat+Data/Finset/Sort): add finiteness and identity theorems for linear orders (#41679) …
Added Infinite.exists_strictMono_or_strictAntiView on Github →