English
Affine independence of p is equivalent to a finite-sum test: for all finite sets s and weights with sum zero, and a corresponding weighted sum, the only solution is the trivial one.
Русский
Аффинная независимость p эквивалентна тесту по суммам: для любых конечных множеств s и весов с суммой нулем, а также при взвешивании точек p, единственное решение нулевое на s.
LaTeX
$$$\\operatorname{AffineIndependent} k p \\iff \\forall s: Finset ι, \\forall w: ι \\to k, (\\sum_{i\\in s} w_i = 0) \\rightarrow (\\sum_{i\\in s} w_i p_i = 0) \\rightarrow (\\forall i\\in s, w_i = 0)$$$
Lean4
/-- Viewing a module as an affine space modelled on itself, we can characterise affine independence
in terms of linear combinations. -/
theorem affineIndependent_iff {ι} {p : ι → V} :
AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0 :=
forall₃_congr fun s w hw => by simp [s.weightedVSub_eq_linear_combination hw]
