English
An indexed family is not linearly independent on s if and only if there exists a Finset-supported finitely supported function f with a nonzero value such that the associated linear combination equals zero.
Русский
Не линейная независимость на s эквивалентна существованию функционала с поддержкой в s, не нулевого на каком−то элементе, для которого линейная комбинация равна нулю.
LaTeX
$$$$\\neg\\operatorname{LinearIndepOn}_R(v,s) \\iff \\exists f : ι \\to R,\\; f\\in \\mathrm{Finsupp.supported}\\,R\\,R\\,s \\wedge \\mathrm{Finsupp.linearCombination}\\,R\\,v\\,f = 0 \\wedge f \\neq 0.$$$$
Lean4
/-- A version of `linearDepOn_iff'` with `Finsupp.linearCombination` unfolded. -/
theorem linearDepOn_iff :
¬LinearIndepOn R v s ↔ ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0 :=
linearDepOn_iff'
