English
If ι is finite, LinearIndependent R v is equivalent to the injectivity of the linear map sending c: ι → R to ∑ i c(i) v(i).
Русский
Если множество индексов ι конечное, линейная независимость семейства v эквивалентна инъективности отображения c: ι → R в сумму ∑ i c(i) v(i).
LaTeX
$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\text{Injective}\\big(\\lambda c:\\iota\\to R.\\sum_{i} c(i)\\,v(i)\\big).$$$$
Lean4
/-- A version of `linearIndepOn_iff` where the linear combination is a `Finset` sum. -/
theorem linearIndepOn_iff' :
LinearIndepOn R v s ↔ ∀ (t : Finset ι) (g : ι → R), (t : Set ι) ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0 :=
by
classical
rw [LinearIndepOn, linearIndependent_iff']
refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
· refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
simp only [Subtype.range_coe_subtype, setOf_mem_eq]
exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
apply h _ _ hit
