English
If a finite set s has equal sums of weights and equal weighted sums of the points, then corresponding weights are equal on s.
Русский
Если для конечного множества s суммы весов равны и взвешенные суммы w_i p_i равны, то веса совпадают на всех элементах s.
LaTeX
$$$\\operatorname{AffineIndependent} k p \\Rightarrow \\operatorname{Eq}\\big(\\sum_{i\\in s} w_1 i\\big)\\;\\big(\\sum_{i\\in s} w_2 i\\big) \\rightarrow \\operatorname{Eq}\\big(\\sum_{i\\in s} w_1 i\\, p_i\\big) \\operatorname{Eq}\\big(\\sum_{i\\in s} w_2 i\\, p_i\\big) \\rightarrow \\forall i\\in s,\\; w_1 i = w_2 i$$$
Lean4
theorem eq_of_sum_eq_sum (hp : AffineIndependent k p) (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i)
(hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i) : ∀ i ∈ s, w₁ i = w₂ i := by
refine fun i hi ↦ sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero (w := w₁ - w₂) ?_ ?_ _ hi) <;>
simpa [sub_mul, sub_smul, sub_eq_zero]
