subset_extendLe — Mathlib

English

If hs is linear independent on s, s ⊆ t, and t spans the whole space, then every element of s lies in the range of Basis.extendLe hs hst ht.

Русский

Если hs линейно независимо на s, s ⊆ t и t порождает всё пространство, то каждый элемент из s принадлежит диапазону Basis.extendLe hs hst ht.

LaTeX

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

Lean4

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

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