Theorems · Theorem · geometry

mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd

∀ {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Nontrivial k] (p : ι → P) (j : ι) (q : P),
  q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j

Given a family of points together with a chosen base point in that family, membership of the affine span of this family corresponds to an identity in terms of weightedVSubOfPoint, with weights that are not required to sum to 1.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsorNontrivial