centerMass_subset — Mathlib

English

If t is a subset of t', and all extra indices carry zero weight, then the center of mass over t equals the center of mass over t'.

Русский

Если t ⊆ t' и новые индексы имеют нулевой вес, то центр массы над t и над t' совпадают.

LaTeX

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

Lean4

theorem centerMass_subset {t' : Finset ι} (ht : t ⊆ t') (h : ∀ i ∈ t', i ∉ t → w i = 0) :
    t.centerMass w z = t'.centerMass w z :=
  by
  rw [centerMass, sum_subset ht h, smul_sum, centerMass, smul_sum]
  apply sum_subset ht
  intro i hit' hit
  rw [h i hit' hit, zero_smul, smul_zero]

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