Commit 2025-12-24 10:09 af65b04c
View on Github →Prove that the diameter of a Euclidean ball is twice its radius. (#32824) feat(Analysis/InnerProductSpace/EuclideanDist): prove that the diameter of a sphere and a ball is twice its radius
All lemmas and theorems: Metric.diam_sphere_eq, Metric.diam_closedBall_eq', Metric.diam_ball_eq. Also, fold a variable declaration inside convexHull_sphere_eq_closedBall.
@Aristotle-Harmonic gave the initial version of the proofs (with many aesops and using v4.24). Leo Mayer and I restructured and cleaned them up.