notMem_span — Mathlib

English

If v is linearly independent on a set s and i is not in s, then v_i is not in the span of {v_j : j ∈ s}.

Русский

Если v линейно независимо на множeстве s и i не принадлежит s, тогда v_i не лежит во span {v_j : j ∈ s}.

LaTeX

$$v_i ∉ span R (v '' s)$$

Lean4

theorem notMem_span (hv : LinearIndepOn R v s) (hi : i ∈ s) : v i ∉ span R (v '' (s \ { i })) := fun hi' ↦
  one_ne_zero <| hv.eq_zero_of_smul_mem_span hi 1 <| by simpa [Set.compl_eq_univ_diff] using hi'

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