English
A family is not linearly independent if and only if there exists a finite subset s ⊆ ι and a nontrivial coefficient function g: ι → R with a nonzero coefficient on some element of s such that ∑ i∈s g(i) v(i) = 0.
Русский
Семейство не линейно независимо тогда и только тогда существует конечное подмножество s ⊆ ι и ненулевые коэффициенты g: ι → R, не все нулевые на s, такие что ∑ i∈s g(i) v(i) = 0.
LaTeX
$$$$\\neg\\operatorname{LinearIndependent}_R(v) \\iff \\exists s:\\mathrm{Finset}\\,\\ι,\\exists g:\\ι\\to R,\\;\\Big(\\sum_{i\\in s} g(i)\\,v(i) = 0\\Big) \\land \\exists i\\in s,\\; g(i)\\neq 0.$$$$
Lean4
theorem not_linearIndependent_iff :
¬LinearIndependent R v ↔ ∃ s : Finset ι, ∃ g : ι → R, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0 :=
by
rw [linearIndependent_iff']
simp only [exists_prop, not_forall]
