sum_affineCombinationLineMapWeights

English

If i and j belong to s, then the sum of affineCombinationLineMapWeights over t ∈ s equals 1: ∑_{t∈s} affineCombinationLineMapWeights i j c t = 1.

Русский

Если i и j принадлежат s, то сумма весов affineCombinationLineMapWeights по t ∈ s равна 1: ∑_{t∈s} affineCombinationLineMapWeights i j c t = 1.

LaTeX

$$$\sum_{t \in s} \operatorname{affineCombinationLineMapWeights}(k,i,j,c,t) = 1$$$

Lean4

@[simp]
theorem sum_affineCombinationLineMapWeights [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (c : k) :
    ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1 :=
  by
  simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
  simp [hi, hj, ← mul_sum]

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