Theorems · Theorem · functional analysis

StrictConvexSpace.of_norm_combo_ne_one

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) →
    StrictConvexSpace ℝ E

Defined in

Mathlib.Analysis.Convex.StrictConvexSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace