subset_span_extend

Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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

← MathLib Explorer

English

t is contained in the span of the extended set.

Русский

t содержится в span расширенного множества.

LaTeX

$$$$t \subseteq \operatorname{span}_K( hs.extend hst ).$$$$

Lean4

theorem subset_span_extend {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) : t ⊆ span K (hs.extend hst) := by
  convert hs.image_subset_span_image_extend hst <;> simp

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

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

Разделы

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

Аффилиация

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