Theorem convexHull_sphere_eq_closedBall

Modification history

2025-12-24 10:09
Mathlib/Analysis/Normed/Module/Convex.lean
Prove that the diameter of a Euclidean ball is twice its radius. (#32824) …
Modified convexHull_sphere_eq_closedBallView on Github →
2025-11-07 20:33
Mathlib/Analysis/Normed/Module/Convex.lean
feat(Analysis.LocallyConvex): a linear map is surjective iff its image contains a ball, or a closed ball, or a sphere (#29033) …
Added convexHull_sphere_eq_closedBallView on Github →