extendLe_subset — Mathlib

English

The extension of hs from s to t yields a basis contained in t; in particular, the range of Basis.extendLe hs hst ht is contained in t.

Русский

Расширение hs с s до t образует базис, состоящий внутри t; следовательно, множество элементов Basis.extendLe hs hst ht содержится в t.

LaTeX

$$$\operatorname{range}(\mathrm{Basis.extendLe}(hs, hst, ht)) \subseteq t$$$

Lean4

theorem extendLe_subset (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    range (Basis.extendLe hs hst ht) ⊆ t :=
  (range_extendLe hs hst ht).symm ▸ hs.extend_subset hst

Похожие утверждения