Theorem not_lt_of_denselyOrdered_of_locallyFinite

Modification history

2025-07-24 19:33
Mathlib/Order/Interval/Finset/Basic.lean
feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)
Added not_lt_of_denselyOrdered_of_locallyFiniteView on Github →