sum_mem — Mathlib

English

The centroid of a finite set coincides with its center of mass using centroid weights.

Русский

Центроид конечного множества совпадает с центром массы, использующим веса центроида.

LaTeX

$$s.centroid R s p = s.centerMass (s.centroidWeights R) p$$

Lean4

theorem sum_mem (hs : Convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) :
    (∑ i ∈ t, w i • z i) ∈ s := by
  simpa only [h₁, centerMass, inv_one, one_smul] using hs.centerMass_mem h₀ (h₁.symm ▸ zero_lt_one) hz

Похожие утверждения