mathlib

6130e571 - feat(topology/metric_space/basic): add some lemmas about spheres (#11719)