of_strictConvex_unitClosedBall — Mathlib

English

If the unit ball is strictly convex, then the ambient normed space is strictly convex.

Русский

Если единичная шаровая окрестность строго выпукла, то окружающее нормированное пространство тоже строго выпукло.

LaTeX

$$$\text{StrictConvexSpace}_{\mathbb{k}} E \text{ if } \overline{B}(0,1) \text{ is strictly convex.}$$$

Lean4

/-- A real normed vector space is strictly convex provided that the unit ball is strictly convex. -/
theorem of_strictConvex_unitClosedBall [LinearMap.CompatibleSMul E E 𝕜 ℝ] (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) :
    StrictConvexSpace 𝕜 E :=
  ⟨fun r hr => by simpa only [smul_unitClosedBall_of_nonneg hr.le] using h.smul r⟩

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