mathlib

e3fac0b5 - refactor(topology/uniform_space/separated): drop `is_separated` (#16458)

refactor(topology/uniform_space/separated): drop `is_separated` (#16458) This predicate is no longer used outside of this file. If we'll need it in the future, then we can redefine it for any topological space in terms of `inseparable`. Also rename `topology.uniform_space.compact_separated` to `topology.uniform_space.compact`.