English
In a finite indexing set, not LinearIndependent is equivalent to the existence of a finite subset t ⊆ s and coefficients with a nonzero coefficient on some i ∈ t.
Русский
В конечном индексе не линейная независимость эквивалентна существованию конечного подмножества t ⊆ s и коэффициентов с ненулевым коэффициентом на некотором i ∈ t.
LaTeX
$$$\neg \text{LinearIndependent } R v \iff \exists t \subseteq s, \exists f, \sum i \in t f_i v_i = \sum i \in s \setminus t f_i v_i \wedge \exists i \in t, 0 < f_i$$$
Lean4
theorem not_linearIndependent_iffₒₛ [DecidableEq ι] [Fintype ι] :
¬LinearIndependent R v ↔ ∃ t, ∃ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∉ t, f i • v i ∧ ∃ i ∈ t, 0 < f i :=
by
simp only [linearIndependent_iffₒₛ, not_forall, pos_iff_ne_zero]
refine ⟨fun ⟨t, f, heq, i, hfi⟩ => ?_, fun ⟨t, f, heq, i, hi, hfi⟩ => ⟨t, f, heq, i, hfi⟩⟩
by_cases hi' : i ∈ t
· exact ⟨t, f, heq, i, hi', hfi⟩
· refine ⟨tᶜ, f, ?_, i, Finset.mem_compl.2 hi', hfi⟩
simp [heq]
