English
A finite family is linearly dependent iff there exist two distinct finite-support linear combinations yielding the same vector.
Русский
Линейно зависимо конечное семейство тогда и только тогда, когда существуют два различных линейных комбинации с конечной опорой, дающие один и тот же вектор.
LaTeX
$$$\\\\neg \\\\mathrm{LinearIndepOn}_R v s \\\\iff \\\\exists f,g : ι \\to_0 R, f \\\\in Finsupp.supported R R s \\\\land \\\\ g \\\\in Finsupp.supported R R s \\\\land Finsupp.linearCombination R v f = Finsupp.linearCombination R v g \\\\land f \\neq g.$$$
Lean4
/-- An indexed set of vectors is linearly dependent iff there are two distinct
`Finsupp.LinearCombination`s of the vectors with the same value. -/
theorem linearDepOn_iff'ₛ :
¬LinearIndepOn R v s ↔
∃ f g : ι →₀ R,
f ∈ Finsupp.supported R R s ∧
g ∈ Finsupp.supported R R s ∧ Finsupp.linearCombination R v f = Finsupp.linearCombination R v g ∧ f ≠ g :=
by simp [linearIndepOn_iffₛ]
