linearIndependent_iff_notMem_span

English

LinearIndependence R v is equivalent to the condition that for every i, a nonzero scalar a cannot produce a nonzero multiple a v(i) lying in the span of the remaining vectors v(j) with j ≠ i.

Русский

Линейная независимость эквивалентна тому, что нет такого i и не нулевого a, чтобы a v(i) ∈ span{v(j): j ≠ i}.

LaTeX

$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\forall i,\\; v(i) \\notin \\operatorname{span}_R\\left( \\{v(j): j \\neq i\\} \\right). $$$$

Lean4

theorem linearIndependent_iff_notMem_span : LinearIndependent K v ↔ ∀ i, v i ∉ span K (v '' (univ \ { i })) :=
  by
  apply linearIndependent_iff_eq_zero_of_smul_mem_span.trans
  constructor
  · intro h i h_in_span
    apply one_ne_zero (h i 1 (by simp [h_in_span]))
  · intro h i a ha
    by_contra ha'
    exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))

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