English
If hv is a linearly independent finite family in M and rank_R M > n, there exists x ∈ M such that Fin.cons x v is linearly independent.
Русский
Если hv — линейно независимая конечная система в M и rank_R M > n, существует x ∈ M такое, что Fin.cons x v линейно независима.
LaTeX
$$$\exists x\, ( \operatorname{LinearIndependent} R (\operatorname{Fin.cons} x\, v) )$$$
Lean4
/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_cons_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M}
(hv : LinearIndependent R v) (h : n < Module.rank R M) : ∃ (x : M), LinearIndependent R (Fin.cons x v) :=
by
obtain ⟨t, h₁, h₂, h₃⟩ := exists_linearIndepOn_of_lt_rank hv.linearIndepOn_id
have : range v ≠ t := by
refine fun e ↦ h.ne ?_
rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂
simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂
obtain ⟨x, hx, hx'⟩ := nonempty_of_ssubset (h₁.ssubset_of_ne this)
exact
⟨x,
(linearIndepOn_id_range_iff (Fin.cons_injective_iff.mpr ⟨hx', hv.injective⟩)).mp
(h₃.mono (Fin.range_cons x v ▸ insert_subset hx h₁))⟩
