Theorems · Theorem · geometry

AffineIndependent.affineCombination_eq_iff_eq

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w₁ w₂ : ι → k} {s : Finset ι},
      ∑ i ∈ s, w₁ i = 1 →
        ∑ i ∈ s, w₂ i = 1 →
          ((Finset.affineCombination k s p) w₁ = (Finset.affineCombination k s p) w₂ ↔ ∀ i ∈ s, w₁ i = w₂ i)

Given an affinely independent family of points, two affine combinations (with sum of weights 1) are equal if and only if their weights are pointwise equal.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Independent

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor