Theorems · Theorem · convex and discrete geometry

sum_mem_ball_of_strictConvexSpace

∀ {V : Type u_2} {ι : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  {t : Finset ι} {w : ι → ℝ} {p : V} {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 ∈ Metric.closedBall p r) → ∑ k ∈ t, w k • z k ∈ Metric.ball p r

Defined in

Mathlib.Analysis.Convex.StrictCombination

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceStrictConvexSpace