Theorems · Theorem · functional analysis

StrictConvexSpace.of_strictConvex_unitClosedBall

∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [LinearMap.CompatibleSMul E E 𝕜 ℝ],
  StrictConvex 𝕜 (Metric.closedBall 0 1) → StrictConvexSpace 𝕜 E

A real normed vector space is strictly convex provided that the unit ball is strictly convex.

Defined in

Mathlib.Analysis.Convex.StrictConvexSpace

Cited by

2 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldPartialOrderNormedAddCommGroupNormedSpaceNormedSpaceLinearMap.CompatibleSMul