affineCombinationLineMapWeights_apply_left

English

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

Русский

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

LaTeX

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

Lean4

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

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