Commit 2026-02-09 08:58 2962adf7

View on Github →

feat: segment is contained in closed ball (#34860)

Estimated changes

Modified Mathlib/Analysis/Normed/Module/Convex.lean

modified theorem convexHull_diam

modified theorem convex_closedBall

added theorem segment_subset_closedBall_left

added theorem segment_subset_closedBall_right