mathlib

5a3abca1 - feat(topology/subset_properties): some compactness properties (#11425)

feat(topology/subset_properties): some compactness properties (#11425) * Add some lemmas about the existence of compact sets * Add `is_compact.eventually_forall_of_forall_eventually` * Some cleanup in `topology/subset_properties` and `topology/separation`