subset_extend

Mathlib.LinearAlgebra.Basis.VectorSpace

URI: https://scilib.ai/kg/mathlib#Module.Basis.subset_extend

English

If hs is a linear independence condition on s, then s is contained in hs.extend (Set.subset_univ _).

Русский

Если hs задаёт линейную независимость на s, то s ⊆ hs.extend(Subset_univ).

LaTeX

$$$s \\subseteq hs.extend (Set.subset_univ\\, _)$$$

Lean4

theorem subset_extend {s : Set V} (hs : LinearIndepOn K id s) : s ⊆ hs.extend (Set.subset_univ _) :=
  hs.subset_extend _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru