mathlib3

6cf5dc53 - feat(topology/support): add lemma `locally_finite.exists_finset_nhd_mul_support_subset` (#13006)

feat(topology/support): add lemma `locally_finite.exists_finset_nhd_mul_support_subset` (#13006) When using a partition of unity to glue together a family of functions, this lemma allows us to pass to a finite family in the neighbourhood of any point. Formalized as part of the Sphere Eversion project.