affineCombinationLineMapWeights_apply_right

English

If i ≠ j, then the weight at t = j is c: affineCombinationLineMapWeights i j c j = c.

Русский

Если i ≠ j, то вес при t = j равен c: affineCombinationLineMapWeights i j c j = c.

LaTeX

$$$\operatorname{affineCombinationLineMapWeights}(k,i,j,c,j) = c$$$

Lean4

@[simp]
theorem affineCombinationLineMapWeights_apply_right [DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) :
    affineCombinationLineMapWeights i j c j = c := by simp [affineCombinationLineMapWeights, h.symm]

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