affineCombinationLineMapWeights_self

English

When the two indices coincide, i = j, the line-map weights reduce to the single-point weights: affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i.

Русский

Когда i = j, веса для lineMap сводятся к весам одной точки: affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i.

LaTeX

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

Lean4

@[simp]
theorem affineCombinationLineMapWeights_self [DecidableEq ι] (i : ι) (c : k) :
    affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i := by
  simp [affineCombinationLineMapWeights]

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