Theorems · Theorem · convex and discrete geometry

norm_sum_lt_of_strictConvexSpace

∀ {V : Type u_2} {ι : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  {t : Finset ι} {w : ι → ℝ} {r : ℝ} {z : ι → V},
  (∀ i ∈ t, 0 ≤ w i) →
    ∑ i ∈ t, w i = 1 →
      ∀ {i j : ι}, i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, ‖z i‖ ≤ r) → ‖∑ k ∈ t, w k • z k‖ < r

Defined in

Mathlib.Analysis.Convex.StrictCombination

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceStrictConvexSpace