English
Not linearIndepOn for a Finset s is equivalent to the existence of a t ⊆ s and f with a nonzero coefficient on some i ∈ t, forming a nontrivial relation.
Русский
Не линейная независимость на финсетe s эквивалентна существованию t ⊆ s и f с ненулевым коэффициентом на i ∈ t, образуя ненулевую зависимость.
LaTeX
$$$\neg LinearIndepOn R v s \iff \exists t \subseteq s, \exists f, \Big( \sum i \in t f_i v_i = \sum i \in s \setminus t f_i v_i \Big) \wedge \exists i \in t, 0 < f_i$$$
Lean4
theorem linearIndepOn_finset_iffₒₛ [DecidableEq ι] {s : Finset ι} :
LinearIndepOn R v s ↔ ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0 :=
by
rw [LinearIndepOn, Fintype.linearIndependent_iffₒₛ]
refine ⟨fun h t ht f heq i hi => h {i | i.1 ∈ t} (f ∘ Subtype.val) ?_ ⟨i, hi⟩, fun h t f heq i => ?_⟩
· simp only [Finset.compl_filter, Finset.sum_filter, Function.comp_apply, Finset.coe_sort_coe]
rw [Finset.sum_coe_sort s fun i => if i ∈ t then f i • v i else 0,
Finset.sum_coe_sort s fun i => if i ∉ t then f i • v i else 0]
simpa [Finset.inter_eq_right.2 ht, Finset.sum_ite, Finset.filter_notMem_eq_sdiff]
· specialize
h (t.map (Embedding.subtype _)) (Finset.map_subtype_subset _) (fun i => if h : i ∈ s then f ⟨i, h⟩ else 0) ?_ i
i.2
· conv =>
enter [2, 1, 1]
rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _
rw [← Finset.map_sdiff]
simpa [Embedding.subtype, ← Finset.compl_eq_univ_sdiff]
simpa using h
