mathlib

168d6ba8 - feat(*/partition_of_unity): more lemmas based on the partition of unity (#15609)

feat(*/partition_of_unity): more lemmas based on the partition of unity (#15609) Add `metric.exists_continuous_real_forall_closed_ball_subset` and `metric.exists_smooth_forall_closed_ball_subset`. For the sphere eversion project, Lemma 3.6.