subset_span_trans

Mathlib.LinearAlgebra.Projectivization.Subspace

URI: https://scilib.ai/kg/mathlib#Projectivization.Subspace.subset_span_trans

English

If S ⊆ span T and T ⊆ span U, then S ⊆ span U.

Русский

Если S ⊆ span T и T ⊆ span U, то S ⊆ span U.

LaTeX

$$$S \subseteq \operatorname{span}(T) \Rightarrow T \subseteq \operatorname{span}(U) \Rightarrow S \subseteq \operatorname{span}(U)$$$

Lean4

theorem subset_span_trans {S T U : Set (ℙ K V)} (hST : S ⊆ span T) (hTU : T ⊆ span U) : S ⊆ span U :=
  gi.gc.le_u_l_trans hST hTU

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

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

Разделы

Аффилиация

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