English
Let p be an affinely independent family and w, w1, w2 be coefficient functions with sums 1 over a finite index set s. If the affine combination w lies in the affine span generated by w1 and w2, and w1 has zero coefficients at i and j while w2 has coefficients of the same sign at i and j, then w has the same sign at i and j.
Русский
Пусть p аффинно независимо, и пусть w, w1, w2 имеют суммы 1. Если w лежит в аффинной оболочке, образованной w1 и w2, и w1 имеет нули на i, j, а w2 имеет коэффициенты одного знака на i и j, тогда w_i и w_j имеют один и тот же знак.
LaTeX
$$$\\text{AffineIndependent}_k(p) \\Rightarrow \\forall s,w,w_1,w_2,\\;\\Big(\\sum_{i\\in s} w_i=1\\Big) \\land \\Big(\\sum_{i\\in s} w_{1,i}=1\\Big) \\land \\Big(\\sum_{i\\in s} w_{2,i}=1\\Big) \\land \\big(w\\in \\operatorname{affineSpan}_k(p)\\big) \\Rightarrow \\forall i,j\\in s,\; w_{1,i}=w_{1,j}=0 \\land \\operatorname{sign}(w_{2,i})=\\operatorname{sign}(w_{2,j}) \\Rightarrow \\operatorname{sign}(w_i)=\\operatorname{sign}(w_j).$$$
Lean4
/-- Given an affinely independent family of points, suppose that an affine combination lies in
the span of two points given as affine combinations, and suppose that, for two indices, the
coefficients in the first point in the span are zero and those in the second point in the span
have the same sign. Then the coefficients in the combination lying in the span have the same
sign. -/
theorem sign_eq_of_affineCombination_mem_affineSpan_pair {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k}
{s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1)
(hs : s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂]) {i j : ι}
(hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0) (hj0 : w₁ j = 0) (hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)) :
SignType.sign (w i) = SignType.sign (w j) :=
by
rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs
rcases hs with ⟨r, hr⟩
rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]
