extend_subset

Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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

← MathLib Explorer

English

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

Русский

Если hs выражает линейную независимость для s, и s ⊆ t, то s ⊆ hs.extend hst.

LaTeX

$$$$s \subseteq hs.extend hst.$$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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