English
A family v_i is not linearly independent if and only if there exists a finite subfamily for which two different coefficient assignments give the same linear combination.
Русский
Семейство векторов {v_i} линейно зависимо тогда и только тогда, когда существует конечное подсемейство, для которого существуют два разных присваивания коэффициентов, дающих одинаковую линейную комбинацию.
LaTeX
$$$\\\\neg \\\\mathrm{LinearIndependent}_R(v) \\\\iff \\\\exists s : \\\\mathrm{Finset} \\\\iota, \\\\exists f,g : \iota \\to R, \\\\sum_{i \\in s} f(i) \\, v_i = \\sum_{i \\in s} g(i) \\, v_i \\\\land \\\\exists i \\in s, f(i) \\neq g(i).$$$
Lean4
theorem not_linearIndependent_iffₛ :
¬LinearIndependent R v ↔
∃ s : Finset ι, ∃ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i :=
by
rw [linearIndependent_iff'ₛ]
simp only [exists_prop, not_forall]
