English
Compact Finset-based reformulation of linear independence with a stand-alone Finset parameter, showing equivalence to standard LI.
Русский
Компактная формулировка через Finset: эквивалентно стандартной LI.
LaTeX
$$$\\operatorname{LinearIndependent}(R,v) \\iff \\forall s:\\operatorname{Finset} ι, \\forall f,g:ι→R, (\\forall i∈s, f_i=g_i) \\Rightarrow (\\sum_{i∈s} f_i v_i)=(\\sum_{i∈s} g_i v_i) \\Rightarrow \\forall i, f_i=g_i$$$
Lean4
theorem linearIndependent_iff''ₛ :
LinearIndependent R v ↔
∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i, f i = g i :=
by
classical
exact
linearIndependent_iff'ₛ.trans
⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his, fun H s f g eq i hi ↦ by
convert
H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
(fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
(by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
exact (if_pos hi).symm⟩
