English
The equivalence and its supporting lemmas give a constructive bijection between a length n+1 independent family and a pair consisting of a length n independent family and an element outside their span.
Русский
Эквивалентность и сопутствующие леммы дают конструкторское биективное соответствие между независимой совокупностью длины n+1 и парой из независимой совокупности длины n и элемента вне их span.
LaTeX
$$$\\text{equiv\_linearIndependent}(n) : \\{ s : Fin(n+1) \\to V \\mid \\operatorname{LinearIndependent}_K s \\} \\cong \\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.init v) ∧ v (Fin.last _) ∉ Submodule.span K (range <| Fin.init v) :=
by rw [← linearIndependent_fin_snoc, Fin.snoc_init_self]
