Theorem Metric.diam_closedBall_eq

Modification history

2025-12-24 10:09
Mathlib/Analysis/Normed/Module/Basic.lean
Prove that the diameter of a Euclidean ball is twice its radius. (#32824) …
Added Metric.diam_closedBall_eqView on Github →