mathlib

27917391 - feat(topology/uniform_space/compact_separated): drop unneeded assumptions (#16457)

feat(topology/uniform_space/compact_separated): drop unneeded assumptions (#16457) Lemmas in this file don't need `[separated_space _]` / `is_separated _` assumption. Also add `nhds_set` versions of some lemmas.