weightedVSub_congr — Mathlib

English

If two weight families w1 and w2 agree on s and two point families p1 and p2 agree on s, then the weightedVSub values coincide.

Русский

Если две семейств весов совпадают на s и две семейств точек совпадают на s, то значения weightedVSub совпадают.

LaTeX

$$$\forall i\in s, w_1(i)=w_2(i),\; p_1(i)=p_2(i)\;\Rightarrow\; s.weightedVSub(p_1,w_1)=s.weightedVSub(p_2,w_2)$$$

Lean4

/-- `weightedVSub` gives equal results for two families of weights and two families of points
that are equal on `s`. -/
theorem weightedVSub_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P} (hp : ∀ i ∈ s, p₁ i = p₂ i) :
    s.weightedVSub p₁ w₁ = s.weightedVSub p₂ w₂ :=
  s.weightedVSubOfPoint_congr hw hp _

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