Theorems · Definition · geometry

Finset.affineCombination

(k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [S : AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → (ι → k) →ᵃ[k] P

A weighted sum of the results of subtracting a default base point from the given points, added to that base point, as an affine map on the weights. This is intended to be used when the sum of the weights is 1, in which case it is an affine combination (barycenter) of the points with the given weights; that condition is specified as a hypothesis on those lemmas that require it.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

159 results in Mathlib

Foundations

Depth 33 from the axioms, rests on 441 definitions · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor