weightedVSubOfPoint_erase — Mathlib

English

Removing a point i from the index set does not affect the sum when the corresponding term is zero (i.e., vsub_self vanishes).

Русский

Удаление элемента из множества индексов не влияет на сумму, если соответствующий член нулевой, например из-за v-перемещения.

LaTeX

$$$ (s \\ {i}).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w $$$

Lean4

/-- The weighted sum is unaffected by removing the base point, if
present, from the set of points. -/
@[simp (high)]
theorem weightedVSubOfPoint_erase [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
    (s.erase i).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w :=
  by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  apply sum_erase
  rw [vsub_self, smul_zero]

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