English
Given hs (independence on s), a subset relation hst: s ⊆ t and ht: ⊤ ≤ span t, the extension hs.extend hst is a basis element of an ambient extension; i.e., Basis.extend hs hst ht .Elem is well-defined.
Русский
Пусть hs — независимость на s, есть включение hst: s ⊆ t и ht: ⊤ ≤ span t; тогда расширение hs.extend hst представляет базисный элемент над расширением.
LaTeX
$$$\\text{ExtendLe} : Basis\\ (hs.extend hst)\\ Elem\\ K\\ V$$$
Lean4
/-- If `s` is a family of linearly independent vectors contained in a set `t` spanning `V`,
then one can get a basis of `V` containing `s` and contained in `t`. -/
noncomputable def extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : Basis (hs.extend hst) K V :=
Basis.mk ((hs.linearIndepOn_extend _).linearIndependent ..)
(le_trans ht <| Submodule.span_le.2 <| by simpa using hs.subset_span_extend hst)
