English
For nontrivial k, a point p1 lies in the affine span of Set.range p if and only if there exist a finite s and weights w with sum 1 such that p1 equals s.affineCombination k p w.
Русский
Для непустого k точка p1 принадлежит афинному span множества Set.range p тогда и только тогда, когда существуют s и веса w, сумма которых равна 1, так что p1 = s.affineCombination k p w.
LaTeX
$$$p_1 \in \affineSpan_k(\Set.range p) \iff \exists s,w, \sum_{i\in s} w_i = 1 \land p_1 = s.affineCombination k p w$$$
Lean4
/-- A point is in the `affineSpan` of an indexed family if and only
if it is an `affineCombination` with sum of weights 1, provided the
underlying ring is nontrivial. -/
theorem mem_affineSpan_iff_eq_affineCombination [Nontrivial k] {p1 : P} {p : ι → P} :
p1 ∈ affineSpan k (Set.range p) ↔ ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 1 ∧ p1 = s.affineCombination k p w :=
by
constructor
· exact eq_affineCombination_of_mem_affineSpan
· rintro ⟨s, w, hw, rfl⟩
exact affineCombination_mem_affineSpan hw p
