English
Let s ⊆ t be subsets of a vector space V over a division ring K, and assume that t spans the whole space (i.e., span_K t = ⊤). If hs is a set on s that is linearly independent, then the range of the extension map Basis.extendLe hs hst ht equals the extended basis hs.extend hst.
Русский
Пусть s ⊆ t — подмножества пространства V над над полем/кольцо K, и предположим, что t образует всё пространство: span_K t = ⊤. Пусть hs является линейно независимым множеством на s. Тогда множество векторов, образованных расширением hs до t, совпадает с базисом hs, расширенным до t.
LaTeX
$$$\operatorname{range}(\mathrm{Basis.extendLe}(hs, hst, ht)) = hs\.extend(hst)$$$
Lean4
theorem range_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
range (Basis.extendLe hs hst ht) = hs.extend hst := by rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]
