dense locally finite orders

Stream: mathlib4

[Aaron Liu]

I was going through the TODOs and noticed

Data/Finset/LocallyFinite: SP: prove that DenselyOrdered + LocallyFinite -> False. Then use this to prove the lemmas that have these assumptions, or try and remove them if possible. Also the one about id_eq - not sure what is meant. (the lemmas near this one can be golfed a tiny bit using le_rfl)

I've proven that DenselyOrdered + LocallyFinite -> ≤ is symmetric, but the conclusion can't be upgraded to False, and I'm not sure what to call this lemma. There are three theorems left which assume both DenselyOrdered and LocallyFiniteOrder, but I can't prove them by exfalso because dense locally finite orders exist. What do I do now? The three theorems assuming dense locally finite orders are

• docs#Finset.nonempty_Ioo
• docs#Finset.Ioo_eq_empty_iff
• docs#Multiset.Ioo_eq_zero_iff

[Bhavik Mehta]

I'm guessing you conclude that the _ < _ relation is always false in a dense locally finite order? And so the rhs of the first lemma should be false, and you can simplify the statement? I'm guessing you can do similar for the others

[Aaron Liu]

That works, but what do I call this lemma? Right now I have _root_.not_lt_of_locallyFiniteOrder_of_denselyOrdered, which seems a bit long.