English
For a finite index set, not LinearIndepOn R v s.toSet is equivalent to the existence of a coefficient function g with a nonzero value on some i in s such that ∑ i∈s g(i) v(i) = 0.
Русский
Для конечного множества индексов не-LI на s эквивалентно существованию коэффициентов g с ненулевым значением на некоторой позиции i в s, для которой ∑ i∈s g(i) v(i) = 0.
LaTeX
$$$$\\neg\\operatorname{LinearIndepOn}_R(v,s.toSet) \\iff \\exists g:\\iota\\to R,\\; \\sum_{i\\in s} g(i)\\,v(i) = 0 \\land \\exists i\\in s,\\; g(i) \\neq 0.$$$$
Lean4
/-- A version of `linearIndepOn_iff` where the linear combination is a `Finset` sum
of a function with support contained in the `Finset`. -/
theorem linearIndepOn_iff'' :
LinearIndepOn R v s ↔
∀ (t : Finset ι) (g : ι → R), (t : Set ι) ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0 :=
by
classical
exact
linearIndepOn_iff'.trans
⟨fun h t g hts htg h0 ↦ h _ _ hts h0, fun h t g hts h0 ↦ by
simpa +contextual [h0] using h t (fun i ↦ if i ∈ t then g i else 0) hts⟩
