subset_extend

Mathlib.LinearAlgebra.LinearIndependent.Lemmas

URI: https://scilib.ai/kg/mathlib#LinearIndepOn.subset_extend

← MathLib Explorer

English

If hs is LIOn on v and s ⊆ t, then hs.extend hst ⊆ t.

Русский

Если hs линейно независим на v и s ⊆ t, то hs.extend hst ⊆ t.

LaTeX

$$$$hs.extend hst \subseteq t.$$$$

Lean4

theorem subset_extend (hs : LinearIndepOn K v s) (hst : s ⊆ t) : s ⊆ hs.extend hst :=
  let ⟨_hbt, hsb, _htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  hsb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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