sum_weightedVSubVSubWeights — Mathlib

English

If i and j belong to a finite set s, then the sum of the weights over t ∈ s is zero: ∑_{t∈s} weightedVSubVSubWeights k i j t = 0.

Русский

Пусть i, j ∈ s; тогда сумма весов по t ∈ s равна нулю: ∑_{t∈s} weightedVSubVSubWeights k i j t = 0.

LaTeX

$$$ \sum_{t \in s} \operatorname{weightedVSubVSubWeights}(k,i,j,t) = 0$$$

Lean4

@[simp]
theorem sum_weightedVSubVSubWeights [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s) :
    ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0 :=
  by
  simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]
  simp [hi, hj]

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