mathlib3

2daeda43 - feat(geometry/euclidean/basic): `dist_center_eq_dist_center_of_mem_sphere'` (#17390)

feat(geometry/euclidean/basic): `dist_center_eq_dist_center_of_mem_sphere'` (#17390) Add a variant of `dist_center_eq_dist_center_of_mem_sphere`, but with the distances the other way round (analogous to the pair of lemmas `mem_sphere` and `mem_sphere'`).