Commit 2022-04-01 22:20 6cf5dc53

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.