exists_linearIndependent_cons_of_lt_finrank

English

Given a LI family v: Fin n → M with n < finrank M, there exists x ∈ M such that v extended by x remains LI.

Русский

Для LI-семьи v: Fin n → M с n < finrank M существует x ∈ M, такое что добавление x сохраняет линейную независимость.

LaTeX

$$$\exists x \in M, \operatorname{LinearIndependent}_R(\mathrm{Fin.snoc}(v,x)).$$$

Lean4

/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_cons_of_lt_finrank {n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v)
    (h : n < finrank R M) : ∃ (x : M), LinearIndependent R (Fin.cons x v) :=
  exists_linearIndependent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h)

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