Theorems · Theorem · convex and discrete geometry

StrictConvex.centerMass_mem_interior

∀ {R : Type u_1} {V : Type u_2} {ι : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup V] [inst_5 : Module R V] {s : Set V} {t : Finset ι} {w : ι → R}
  {z : ι → V},
  StrictConvex R s →
    (∀ i ∈ t, 0 ≤ w i) →
      ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s

Defined in

Mathlib.Analysis.Convex.StrictCombination

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingTopologicalSpaceAddCommGroupModule