weightedVSubOfPoint_vadd — Mathlib

English

Translating all points by a vector v and adjusting the base point accordingly does not change the weighted sum: s.weightedVSubOfPoint (v + p) b w = s.weightedVSubOfPoint p (-v + b) w.

Русский

Сдвиг всех точек на вектор v и надстройка базовой точки не меняют взвешенную сумму: s.weightedVSubOfPoint (v+p) b w = s.weightedVSubOfPoint p (b−v) w.

LaTeX

$$$ s.weightedVSubOfPoint (v + p) b w = s.weightedVSubOfPoint p (-v + b) w $$$

Lean4

theorem weightedVSubOfPoint_vadd (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (v : V) :
    s.weightedVSubOfPoint (v +ᵥ p) b w = s.weightedVSubOfPoint p (-v +ᵥ b) w := by
  simp [vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm]

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