English
If w1 and w2 agree outside a distinguished index j, then s.weightedVSubOfPoint p (p_j) w1 = s.weightedVSubOfPoint p (p_j) w2.
Русский
Если веса w1 и w2 совпадают за пределами индекса j, то вычисления weightedVSubOfPoint с базовой точкой p_j совпадают.
LaTeX
$$$ \\text{If } w_1(i)=w_2(i) \\text{ for all } i \\ne j, \\text{ then } s.weightedVSubOfPoint(p,(p_j)) w_1 = s.weightedVSubOfPoint(p,(p_j)) w_2 $$$
Lean4
/-- Given a family of points, if we use a member of the family as a base point, the
`weightedVSubOfPoint` does not depend on the value of the weights at this point. -/
theorem weightedVSubOfPoint_eq_of_weights_eq (p : ι → P) (j : ι) (w₁ w₂ : ι → k) (hw : ∀ i, i ≠ j → w₁ i = w₂ i) :
s.weightedVSubOfPoint p (p j) w₁ = s.weightedVSubOfPoint p (p j) w₂ :=
by
simp only [Finset.weightedVSubOfPoint_apply]
congr
ext i
rcases eq_or_ne i j with h | h
· simp [h]
· simp [hw i h]
