feat(topology/*): add lemmas about `𝓝[⋃ i, s i] a` (#18321)
* Add `theorem nhds_within_eq_nhds`, `nhds_within_bUnion`, `nhds_within_sUnion`, `nhds_within_Union`, `nhds_within_inter_of_mem'`.
* Add `locally_finite.nhds_within_Union`, use it to golf `locally_finite.is_closed_Union` and `locally_finite.closure_Union`.
* Reformulate `continuous_subtype_nhds_cover` in terms of `continuous_on`, rename to `continuous_of_cover_nhds`.
* Reformulate `continuous_subtype_is_closed_cover` in terms of `continuous_on`, several versions are named `locally_finite.continuous_on_Union`, `locally_finite.continuous`, and primed versions of these lemmas.
* Reorder imports.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
