English
With decidable equality, not LinearIndepOn is equivalent to the existence of a t ⊆ s, a coefficient function f, and a nontrivial relation with a nonzero coefficient.
Русский
При разрешаемом равенстве не-линейная независимость на финсетe эквивалентна существованию t ⊆ s, коэффициентов f и ненулевой зависимости.
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 not_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 ∈ t, 0 < f i :=
by
simp only [linearIndepOn_finset_iffₒₛ, not_forall, pos_iff_ne_zero]
refine ⟨fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ?_, fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ⟨t, hst, f, heq, i, hst hi, hfi⟩⟩
by_cases hi' : i ∈ t
· exact ⟨t, hst, f, heq, i, hi', hfi⟩
· refine ⟨s \ t, Finset.sdiff_subset, f, ?_, i, Finset.mem_sdiff.2 ⟨hi, hi'⟩, hfi⟩
simpa [Finset.sdiff_sdiff_eq_self hst] using heq.symm
