Mathlib Changelog
v4
Changelog
About
Github
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