English
Let v: ι → M be a family. Linear independence over R is equivalent to the statement that if a linear combination ∑ i∈s g(i) v(i) vanishes for every finite s with the condition that g vanishes outside s, then all coefficients g(i) are zero.
Русский
Пусть v : ι → M. Линейная независимость по R эквивалентна тому, что если для любого конечного подмножества s ⊆ ι существует линейная комбинация ∑ i∈s g(i) v(i) = 0 с условием, что g(i) = 0 вне s, то все коэффициенты g(i) равны нулю.
LaTeX
$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\forall (s : \\mathrm{Finset}\\,\\ι) (g : \\ι \\to R),\\; (\\forall i \\notin s,\\; g(i) = 0) \\rightarrow \\Big(\\sum_{i\\in s} g(i) \\cdot v(i) = 0 \\rightarrow \\forall i,\\; g(i) = 0\\Big).$$$$
Lean4
/-- A version of `linearIndependent_iff` where the linear combination is a `Finset` sum
of a function with support contained in the `Finset`. -/
theorem linearIndependent_iff'' :
LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ i, g i = 0 :=
by
classical
exact
linearIndependent_iff'.trans
⟨fun H s g hg hv i => if his : i ∈ s then H s g hv i his else hg i his, fun H s g hg i hi =>
by
convert
H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
(by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i
exact (if_pos hi).symm⟩
