Theorem Set.Subsingleton.denselyOrdered

Modification history

2025-07-24 19:33
Mathlib/Data/Set/Subsingleton.lean
feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)
Added Set.Subsingleton.denselyOrderedView on Github →