English
If a finite set t in V is not affinely independent, there exists a nontrivial linear relation with sum of coefficients zero and a point with nonzero coefficient.
Русский
Если конечное множество векторного пространства не является аффинно независимым, то существует нетривиальная линейная зависимость с суммой коэффициентов нулевой и с не нулевым коэффициентом у некоторой точки.
LaTeX
$$$\\forall t: Finset V,\\; \\neg\\operatorname{AffineIndependent} k p\\;\\Rightarrow\\; \\exists f: V\\to k,\\; \\sum_{e\\in t} f(e) e = 0 \\land \\sum_{e\\in t} f(e) = 0 \\land \\exists x\\in t, f(x) \\neq 0$$$
Lean4
theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {t : Finset V} (h : ¬AffineIndependent k ((↑) : t → V)) :
∃ f : V → k, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0 := by
classical
rw [affineIndependent_iff_of_fintype] at h
simp only [exists_prop, not_forall] at h
obtain ⟨w, hw, hwt, i, hi⟩ := h
simp only [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w ((↑) : t → V) hw 0, vsub_eq_sub,
Finset.weightedVSubOfPoint_apply, sub_zero] at hwt
let f : ∀ x : V, x ∈ t → k := fun x hx => w ⟨x, hx⟩
refine ⟨fun x => if hx : x ∈ t then f x hx else (0 : k), ?_, ?_, by use i; simp [f, hi]⟩
on_goal 1 =>
suffices (∑ e ∈ t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0
by
convert this
rename V => x
by_cases hx : x ∈ t <;> simp [hx]
all_goals simp only [f, Finset.sum_dite_of_true fun _ h => h, Finset.mk_coe, hwt, hw]
