English
For any finite subset s ⊆ ι, LinearIndepOn R v s is equivalent to the condition that if a finite linear combination ∑ i∈s g(i) v(i) equals 0, then g(i) = 0 for all i ∈ s.
Русский
Для любого конечного подмножества s ⊆ ι линейная независимость на s эквивалентна условиям: если линейная комбинация ∑ i∈s g(i) v(i) = 0, то все g(i) равны нулю.
LaTeX
$$$$\\operatorname{LinearIndepOn}_R(v,s) \\iff \\forall g:\\iota\\to R,\\; \\Big(\\sum_{i\\in s} g(i)\\,v(i) = 0 \\Rightarrow \\forall i\\in s,\\; g(i)=0\\Big).$$$$
Lean4
theorem linearIndepOn_finset_iff {s : Finset ι} :
LinearIndepOn R v s ↔ ∀ f : ι → R, ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0 := by
classical
simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
constructor
· rintro hv f hf i hi
rw [← s.sum_attach] at hf
exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩
· rintro hv f hf₀ i
simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) i
