not_linearIndepOn_finset_iff — Mathlib

English

For a finite subset s ⊆ ι, not LinearIndepOn R v s is equivalent to the existence of a nontrivial linear relation ∑ i∈s g(i) v(i) = 0 with some g(i) ≠ 0.

Русский

Для конечного подмножества s ⊆ ι существование ненулевой линейной зависимости на v ограничено кратной суммой g(i) v(i) = 0.

LaTeX

$$$$\\neg\\operatorname{LinearIndepOn}_R(v,s) \\iff \\exists g:\\iota\\to R,\\; \\Big(\\sum_{i\\in s} g(i)\\,v(i) = 0\\Big) \\land \\exists i\\in s,\\; g(i) \\neq 0.$$$$

Lean4

theorem not_linearIndepOn_finset_iff {s : Finset ι} :
    ¬LinearIndepOn R v s ↔ ∃ f : ι → R, ∑ i ∈ s, f i • v i = 0 ∧ ∃ i ∈ s, f i ≠ 0 := by
  simpa using linearIndepOn_finset_iff.not

Похожие утверждения