English
Equivalence between the set of length n+1 linearly independent vectors and the pair consisting of a length n independent family and a vector outside the span of its range.
Русский
Эквивалентность между множеством линейно независимых векторoв длины n+1 и парой: независимая совокупность длины n и вектор вне их порождающего пространства.
LaTeX
$$$\{ s : Fin(n+1) \to V \mid \operatorname{LinearIndependent}_K s \} \simeq \Sigma s : \{ t : Fin n \to V \mid \operatorname{LinearIndependent}_K t \}, ((\operatorname{span}_K(\operatorname{range}(s)))^{\complement} : Set V)$$$
Lean4
theorem linearIndependent_fin_succ {n} {v : Fin (n + 1) → V} :
LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (range <| Fin.tail v) := by
rw [← linearIndependent_fin_cons, Fin.cons_self_tail]
