English
A family restricted to a finite set s is linearly independent if and only if, for any two coefficient functions f,g with sum over s equal, we have f(i)=g(i) for all i in s.
Русский
Семейство, ограниченное конечным множеством s, линейно независимо тогда и только тогда, когда для любых двух коэффициентов f,g на s равенство сумм приводит к равенству коэффициентов на каждом i∈s.
LaTeX
$$$\\\\mathrm{LinearIndepOn}_R(v,s) \\\\iff \\\\forall f,g : \\iota \\to R, \\\\Big( \\\\sum_{i \\\\in s} f(i) \\, v_i = \\\\sum_{i \\\\in s} g(i) \\, v_i \\\\Rightarrow \\\\forall i \\\\in s, f(i)=g(i) \\\\Big).$$$
Lean4
theorem linearIndepOn_finset_iffₛ {s : Finset ι} :
LinearIndepOn R v s ↔ ∀ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i := by
classical
simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
constructor
· rintro hv f g hfg i hi
simp_rw [← s.sum_attach] at hfg
exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
· rintro hv f g hfg i
simpa using
hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0) (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0)
(by simpa +contextual [← s.sum_attach]) i
