linearIndependent_fin_cons — Mathlib

English

For a finite sequence v: Fin n → V, linear independence of v implies linear independence of Fin.cons x v provided x is outside span of range v.

Русский

Для конечной последовательности v: Fin n → V независимость v влечет независимость Fin.cons x v, если x выходит за пределы span range v.

LaTeX

$$$\operatorname{LinearIndependent}_K(v) \Rightarrow \bigl( x \notin \operatorname{span}_K(\operatorname{range} v) \Rightarrow \operatorname{LinearIndependent}_K(\operatorname{Fin.cons} x\,v) \bigr)$$$

Lean4

theorem linearIndependent_fin_cons {n} {v : Fin n → V} :
    LinearIndependent K (Fin.cons x v : Fin (n + 1) → V) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (range v) :=
  by
  rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]
  exact Iff.rfl

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