feat(topology/subset_properties): variant of elim_nhds_subcover for compact_space (#7304)
feat(topology/subset_properties): variant of elim_nhds_subcover for compact_space (#7304)

I put this in the `compact_space` namespace, although dot notation won't work so if preferred I can move it back to `_root_`.




Co-authored-by: Scott Morrison <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib