Theorem WithTop.denselyOrdered_set_iff_subsingleton

Modification history

2026-09-04 09:44
Mathlib/Order/Interval/Finset/DenselyOrdered.lean
chore(Order/WithBot): remove defeq between `WithBot.LE`/`LT` and `WithTop.LE`/`LT` (#42622) …
Deleted WithTop.denselyOrdered_set_iff_subsingletonView on Github →
2025-07-24 19:33
Mathlib/Order/Interval/Finset/DenselyOrdered.lean
feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)
Added WithTop.denselyOrdered_set_iff_subsingletonView on Github →