Theorem WithTop.denselyOrdered_iff

Modification history

2025-12-24 15:23
Mathlib/Order/WithBot.lean
chore(Order/WithBot): add `to_dual` attributes (part 3) (#32499) …
Modified WithTop.denselyOrdered_iffView on Github →
2025-07-24 19:33
Mathlib/Order/WithBot.lean
feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)
Added WithTop.denselyOrdered_iffView on Github →