English
If two weight families w1, w2 agree on s and two point families p1, p2 agree on s, then the corresponding weightedVSubOfPoint values coincide for the same base point b.
Русский
Если пары весов w1, w2 совпадают на s и пары точек p1, p2 совпадают на s, то значения weightedVSubOfPoint совпадают при том же базовом b.
LaTeX
$$$ (hw) \\to s.weightedVSubOfPoint(p_1,b,w_1) = s.weightedVSubOfPoint(p_2,b,w_2) $ под условиями hw, hp.$$
Lean4
/-- `weightedVSubOfPoint` gives equal results for two families of weights and two families of
points that are equal on `s`. -/
theorem weightedVSubOfPoint_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
(hp : ∀ i ∈ s, p₁ i = p₂ i) (b : P) : s.weightedVSubOfPoint p₁ b w₁ = s.weightedVSubOfPoint p₂ b w₂ :=
by
simp_rw [weightedVSubOfPoint_apply]
refine sum_congr rfl fun i hi => ?_
rw [hw i hi, hp i hi]
