English
Affine combinations preserve a weak betweenness: if certain affine combinations sum to 1 and the corresponding weight entries satisfy a betweenness condition, then the affine combinations themselves satisfy a weak betweenness relation.
Русский
Афинные сочетания сохраняют слабое отношение между точками: если заданные веса суммируются в единицу, и соответствующие элементы удовлетворяют условию междуности, то сами аффинные комбинации удовлетворяют слабому betw.
LaTeX
$$$AffineIndependent\\ R\\ p \\Rightarrow \\Big( hw: \\sum_{i\\in s} w_i = 1\\Big) \\land \\Big( \\sum_{i\\in s} w_1i = 1 \\Big) \\land \\Big( \\sum_{i\\in s} w_2i = 1 \\Big) \\Rightarrow Sbtw(R, s.affineCombination(R,p,w_1), s.affineCombination(R,p,w), s.affineCombination(R,p,w_2))$$$
Lean4
theorem affineCombination_of_mem_affineSpan_pair [NoZeroDivisors R] [NoZeroSMulDivisors R V] {ι : Type*} {p : ι → P}
(ha : AffineIndependent R p) {w w₁ w₂ : ι → R} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1)
(hw₂ : ∑ i ∈ s, w₂ i = 1)
(h : s.affineCombination R p w ∈ line[R, s.affineCombination R p w₁, s.affineCombination R p w₂]) {i : ι}
(his : i ∈ s) (hs : Sbtw R (w₁ i) (w i) (w₂ i)) :
Sbtw R (s.affineCombination R p w₁) (s.affineCombination R p w) (s.affineCombination R p w₂) :=
by
rw [affineCombination_mem_affineSpan_pair ha hw hw₁ hw₂] at h
rcases h with ⟨r, hr⟩
rw [hr i his, sbtw_mul_sub_add_iff] at hs
change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr
rw [s.affineCombination_congr hr fun _ _ => rfl]
rw [← s.weightedVSub_vadd_affineCombination, s.weightedVSub_const_smul, ← s.affineCombination_vsub, ← lineMap_apply,
sbtw_lineMap_iff, and_iff_left hs.2, ← @vsub_ne_zero V, s.affineCombination_vsub]
intro hz
have hw₁w₂ : (∑ i ∈ s, (w₁ - w₂) i) = 0 := by simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
refine hs.1 ?_
have ha' := ha s (w₁ - w₂) hw₁w₂ hz i his
rwa [Pi.sub_apply, sub_eq_zero] at ha'
