English
In a strictly convex normed space, every closed ball is strictly convex.
Русский
В строго выпуклом нормированном пространстве каждое замкнутое шар является строговыпуклым.
LaTeX
$$$\text{StrictConvex}_{\mathbb{k}}(\overline{B}(x,r))$$$
Lean4
/-- A closed ball in a strictly convex space is strictly convex. -/
theorem strictConvex_closedBall [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ) : StrictConvex 𝕜 (closedBall x r) :=
by
rcases le_or_gt r 0 with hr | hr
· exact (subsingleton_closedBall x hr).strictConvex
rw [← vadd_closedBall_zero]
exact (StrictConvexSpace.strictConvex_closedBall r hr).vadd _