weightedVSubOfPoint_const_smul — Mathlib

English

Explicit evaluation: the linear map equals the finite sum ∑ w_i (p_i − b).

Русский

Явная оценка: линейное отображение равно ∑ w_i (p_i − b).

LaTeX

$$$ (s.weightedVSubOfPoint p b) w = \\sum_{i \\in s} w_i (p_i - b)$$$

Lean4

/-- A constant multiplier of the weights in `weightedVSubOfPoint` may be moved outside the
sum. -/
theorem weightedVSubOfPoint_const_smul (w : ι → k) (p : ι → P) (b : P) (c : k) :
    s.weightedVSubOfPoint p b (c • w) = c • s.weightedVSubOfPoint p b w := by
  simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]

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