mathlib

f40cd3cf - feat(topology/algebra/order/basic): in a second-countable linear order, only countably many points are isolated to the right (#14564)

feat(topology/algebra/order/basic): in a second-countable linear order, only countably many points are isolated to the right (#14564) This makes it possible to remove a useless `densely_ordered` assumption in a lemma in `borel_space`.