weightedVSubVSubWeights_apply_of_ne

English

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

Русский

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

LaTeX

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

Lean4

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

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