English
If v is a linearly independent family, then Basis.sumExtend hs is a basis of V indexed by ι ⊕ sumExtendIndex hs, obtained by extending v with the new vectors.
Русский
Пусть v — линейно независимая семейство; тогда Basis.sumExtend hs является базисом V, индексированным ι ⊕ sumExtendIndex hs, полученным добавлением новых векторов.
LaTeX
$$$\\text{sumExtend} : Basis\\ (ι \\oplus \\text{sumExtendIndex}\\, hs)\\ K\\ V$$$
Lean4
/-- If `v` is a linear independent family of vectors, extend it to a basis indexed by a sum type. -/
noncomputable def sumExtend (hs : LinearIndependent K v) : Basis (ι ⊕ sumExtendIndex hs) K V :=
let s := Set.range v
let e : ι ≃ s := Equiv.ofInjective v hs.injective
let b := hs.linearIndepOn_id.extend (subset_univ (Set.range v))
(Basis.extend hs.linearIndepOn_id).reindex <|
Equiv.symm <|
calc
ι ⊕ (b \ s : Set V) ≃ s ⊕ (b \ s : Set V) := Equiv.sumCongr e (Equiv.refl _)
_ ≃ b :=
haveI := Classical.decPred (· ∈ s)
Equiv.Set.sumDiffSubset (hs.linearIndepOn_id.subset_extend _)
