mathlib

e0c0d84a - feat(topology/separation): removing a finite set from a dense set preserves density (#10405)

feat(topology/separation): removing a finite set from a dense set preserves density (#10405) Also add the fact that one can find a dense set containing neither top nor bottom in a nontrivial dense linear order.