not_linearIndepOn_finset_iffₛ — Mathlib

English

The negation of linear independence over a finite set s is equivalent to the existence of two distinct coefficient functions with equal finite linear combinations on s.

Русский

Отрицание линейной независимости над конечным множеством s эквивалентно существованию двух различных коэффициентов, дающих одинаковую линейную комбинацию на s.

LaTeX

$$$\\\\neg \\\\mathrm{LinearIndepOn}_R(v,s) \\\\iff \\\\exists f,g : \ι \\to R, \\\\sum_{i \\\\in s} f(i) \\, v_i = \\\\sum_{i \\\\in s} g(i) \\, v_i \\\\land \\\\exists i \\\\in s, f(i) \ne g(i).$$$

Lean4

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

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