weightedVSubOfPoint_insert — Mathlib

English

Inserting a new index i into the finite set does not change the weighted sum relative to p_i: (insert i s).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w.

Русский

Вставка нового индекса i в множество не изменяет взвешенную сумму относительно p_i.

LaTeX

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

Lean4

/-- The weighted sum is unaffected by adding the base point, whether
or not present, to the set of points. -/
@[simp (high)]
theorem weightedVSubOfPoint_insert [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
    (insert i s).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w :=
  by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  apply sum_insert_zero
  rw [vsub_self, smul_zero]

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