centerMass_of_sum_add_sum_eq_zero

English

If the sums of two finite index sets of weights cancel to zero, then their centers of mass are equal.

Русский

Если суммы весов по двум конечным наборам равны нулю, то их центры масс совпадают.

LaTeX

$$s.centerMass\, w\, z = t.centerMass\, w\, z$$

Lean4

theorem centerMass_of_sum_add_sum_eq_zero {s t : Finset ι} (hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0)
    (hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0) : s.centerMass w z = t.centerMass w z := by
  simp [centerMass, eq_neg_of_add_eq_zero_right hw, eq_neg_of_add_eq_zero_left hz]

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