English
The function defining the extended basis equals the natural inclusion. The map from the extended basis to the ambient module is the identity on the underlying set.
Русский
Функция, задающая расширенный базис, совпадает с естественным включением. Отображение с расширенного базиса в исходный модуль есть тождественное на множестве.
LaTeX
$$$\\iota$-indexed extension equals identity: \\ (Basis.extend hs hst ht) = id$$
Lean4
/-- If `s` is a linear independent set of vectors, we can extend it to a basis. -/
noncomputable def extend (hs : LinearIndepOn K id s) : Basis (hs.extend (subset_univ s)) K V :=
Basis.mk (hs.linearIndepOn_extend _).linearIndependent_restrict
(SetLike.coe_subset_coe.mp <| by simpa using hs.subset_span_extend (subset_univ s))
