weightedVSubOfPoint_apply_const — Mathlib

English

If all points p_i equal a fixed point p, then the weighted V-subsum equals (sum of weights) times (p − b).

Русский

Если все точки p_i равны фиксированной точке p, то взвешенная сумма равна (сумма весов) умножить на (p − b).

LaTeX

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

Lean4

/-- The value of `weightedVSubOfPoint`, where the given points are equal. -/
@[simp (high)]
theorem weightedVSubOfPoint_apply_const (w : ι → k) (p : P) (b : P) :
    s.weightedVSubOfPoint (fun _ => p) b w = (∑ i ∈ s, w i) • (p -ᵥ b) := by rw [weightedVSubOfPoint_apply, sum_smul]

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