Commit 2025-07-24 19:33 69f3dbf3

View on Github →

feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Subsingleton.lean

added theorem Set.Subsingleton.denselyOrdered

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem Int.not_denselyOrdered

added theorem WithZero.denselyOrdered_iff

added theorem WithZero.denselyOrdered_set_iff_subsingleton

added theorem denselyOrdered_additive_iff

added theorem denselyOrdered_multiplicative_iff

added theorem not_denselyOrdered_withZero_int

Modified Mathlib/Order/Interval/Finset/Basic.lean

added theorem not_lt_of_denselyOrdered_of_locallyFinite

Created Mathlib/Order/Interval/Finset/DenselyOrdered.lean

added theorem LocallyFiniteOrder.denselyOrdered_iff_subsingleton

added theorem WithBot.denselyOrdered_set_iff_subsingleton

added theorem WithTop.denselyOrdered_set_iff_subsingleton

added theorem denselyOrdered_set_iff_subsingleton

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.denselyOrdered_iff

added theorem WithTop.denselyOrdered_iff