centerMass_eq_of_sum_1

Mathlib.Analysis.Convex.Combination

URI: https://scilib.ai/kg/mathlib#Finset.centerMass_eq_of_sum_1

← MathLib Explorer

English

CenterMass is invariant under negating all weights: t.centerMass(−w) z = t.centerMass w z.

Русский

Центр массы не зависит от знака всех весов: центрмасса(−w) = центрмасса(w).

LaTeX

$$$t.centerMass(-w, z) = t.centerMass(w, z).$$$

Lean4

theorem centerMass_eq_of_sum_1 (hw : ∑ i ∈ t, w i = 1) : t.centerMass w z = ∑ i ∈ t, w i • z i := by
  simp only [Finset.centerMass, hw, inv_one, one_smul]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru