notMem_span_of_insert — Mathlib

English

If a vector v_i becomes dependent after inserting i into s, i.e., a v_i lies in span(v''s), then a=0.

Русский

Если добавление i в s делает зависимым, и a v_i лежит во span {v_j: j ∈ s}, то a=0.

LaTeX

$$$hv.eq_zero_of_smul_mem_span (i) (a) (ha)$ equivalently: if $a v_i \in span R (v '' (s))$ then $a=0$.$$

Lean4

theorem notMem_span_of_insert (hv : LinearIndepOn R v (insert i s)) (hi : i ∉ s) : v i ∉ span R (v '' s) := by
  simpa [hi] using hv.notMem_span <| mem_insert ..

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