affineCombinationLineMapWeights — Mathlib

English

The affine weights used to express line maps are defined by the lineMap-weighting: affineCombinationLineMapWeights k i j c is the sum of c times weightedVSubVSubWeights k j i plus affineCombinationSingleWeights k i.

Русский

Афинные веса для выражения линейного отображения задаются через lineMap: affineCombinationLineMapWeights k i j c = c · weightedVSubVSubWeights k j i + affineCombinationSingleWeights k i.

LaTeX

$$$\text{affineCombinationLineMapWeights}(k,i,j,c) = c \cdot \operatorname{weightedVSubVSubWeights}(k,j,i) + \operatorname{affineCombinationSingleWeights}(k,i)$$$

Lean4

/-- Weights for expressing `lineMap` as an affine combination. -/
def affineCombinationLineMapWeights [DecidableEq ι] (i j : ι) (c : k) : ι → k :=
  c • weightedVSubVSubWeights k j i + affineCombinationSingleWeights k i

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