English
The negation of linear independence over a finite set s is equivalent to the existence of two distinct coefficient functions with equal finite linear combinations on s.
Русский
Отрицание линейной независимости над конечным множеством s эквивалентно существованию двух различных коэффициентов, дающих одинаковую линейную комбинацию на s.
LaTeX
$$$\\\\neg \\\\mathrm{LinearIndepOn}_R(v,s) \\\\iff \\\\exists f,g : \ι \\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) \ne g(i).$$$
Lean4
theorem not_linearIndepOn_finset_iffₛ {s : Finset ι} :
¬LinearIndepOn R v s ↔ ∃ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i := by
simpa using linearIndepOn_finset_iffₛ.not