mathlib3

398027d5 - feat(topology/subset_properties): add `countable_cover_nhds_within_of_sigma_compact` (#8350)

feat(topology/subset_properties): add `countable_cover_nhds_within_of_sigma_compact` (#8350) This is a version of `countable_cover_nhds_of_sigma_compact` for a covering of a closed set instead of the whole space. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>