English
An affine combination lying in the affine span of two affine combinations is equivalent to a parameterized description along a line through those two combinations.
Русский
Аффинная комбинация, лежащая в аффинной оболочке пары аффинных комбинаций, эквивалентна параметрическому описанию по линии между этими двумя комбинациями.
LaTeX
$$$\\forall ha:\\operatorname{AffineIndependent} k p, \\forall {w,w_1,w_2},\\; Eq(\\sum_{i\\in s} w i)=1,\\ Eq(\\sum w_1 i)=1,\\ Eq(\\sum w_2 i)=1 \\Rightarrow\\; \\text{равенство индикаторов} \\Rightarrow \\exists r: k, \\forall i\\in s, w_i = r (w_2 i - w_1 i) + w_1 i$$$
Lean4
/-- Given an affinely independent family of points, an affine combination lies in the
span of two points given as affine combinations if and only if it is an affine combination
with weights those of one point plus a multiple of the difference between the weights of the
two points. -/
theorem affineCombination_mem_affineSpan_pair {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k} {s : Finset ι}
(_ : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) :
s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂] ↔
∃ r : k, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i :=
by
rw [← vsub_vadd (s.affineCombination k p w) (s.affineCombination k p w₁),
AffineSubspace.vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
s.affineCombination_vsub, Set.pair_comm, weightedVSub_mem_vectorSpan_pair h _ hw₂ hw₁]
· simp only [Pi.sub_apply, sub_eq_iff_eq_add]
· simp_all only [Pi.sub_apply, Finset.sum_sub_distrib, sub_self]
