Linear locally finite orders are densely ordered iff they are trivial

Main results

• LocallyFiniteOrder.denselyOrdered_iff_subsingleton: A linear locally finite order is densely ordered if and only if it is a subsingleton.

theorem LocallyFiniteOrder.denselyOrdered_iff_subsingleton {X : Type u_1} [LinearOrder X] [LocallyFiniteOrder X] : DenselyOrdered X ↔ Subsingleton X

theorem denselyOrdered_set_iff_subsingleton {X : Type u_1} [LinearOrder X] [LocallyFiniteOrder X] {s : Set X} : DenselyOrdered ↑s ↔ s.Subsingleton

theorem WithBot.denselyOrdered_set_iff_subsingleton {X : Type u_1} [LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithBot X)} : DenselyOrdered ↑s ↔ s.Subsingleton

theorem WithTop.denselyOrdered_set_iff_subsingleton {X : Type u_1} [LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithTop X)} : DenselyOrdered ↑s ↔ s.Subsingleton