Theorem segment_subset_closedBall_left

Modification history

2026-02-09 08:58
Mathlib/Analysis/Normed/Module/Convex.lean
feat: segment is contained in closed ball (#34860)
Added segment_subset_closedBall_leftView on Github →