Commit 2023-03-25 17:27 55d771df

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.