English
A finite-setup version: Not LinearIndependent is equivalent to the existence of finite s,t,f with a nontrivial relation between sums and a positive coefficient.
Русский
Для конечного случая не-линейная независимость эквивалентна существованию конечных s,t,f, дающих ненулевую линейную зависимость.
LaTeX
$$$\neg \text{LinearIndependent } R v \iff \exists (s t : Finset ι) (f : ι \to R), Disjoint s t \wedge \sum i \in s, f_i v_i = \sum i \in t, f_i v_i \wedge \exists i \in s, 0 < f_i$$$
Lean4
nonrec theorem linearIndependent_iffₒₛ [DecidableEq ι] [Fintype ι] :
LinearIndependent R v ↔ ∀ t, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∉ t, f i • v i → ∀ i, f i = 0 :=
by
rw [linearIndependent_iffₒₛ]
refine ⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩
· specialize h t tᶜ f disjoint_compl_right heq
by_cases hi : i ∈ t
· exact h.1 i hi
· exact h.2 i (Finset.mem_compl.2 hi)
· specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
· rw [← Finset.sum_subset ht₁t₂.le_compl_left]
· convert heq using 2 with i hi i hi <;> simp [hi]
· intro i hi hi'
simp [Finset.mem_compl.1 hi, hi']
refine ⟨fun i hi => ?_, fun i hi => ?_⟩ <;> simpa [hi] using h i
