affineCombinationLineMapWeights_apply_of_ne

English

If t is different from both i and j (t ≠ i and t ≠ j), then the weight is zero: affineCombinationLineMapWeights i j c t = 0.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem affineCombinationLineMapWeights_apply_of_ne [DecidableEq ι] {i j t : ι} (hi : t ≠ i) (hj : t ≠ j) (c : k) :
    affineCombinationLineMapWeights i j c t = 0 := by simp [affineCombinationLineMapWeights, hi, hj]

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