notMem_span — Mathlib

English

For a linearly independent family, no vector v_i lies in the span of the others; equivalently v_i cannot be written as a nontrivial linear combination of the others.

Русский

Для линейно независимого семейства вектор v_i не лежит во span остальных; эквивалентно невозможности выразить v_i как не тривиальную лин. комбинацию остальных.

LaTeX

$$v_i ∉ span R (v '' (univ \ { i }))$$

Lean4

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

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