strictConvex_closedBall — Mathlib

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 _

Похожие утверждения