span_le_span

Mathlib.LinearAlgebra.Projectivization.Subspace

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

English

If S ⊆ T then span S ≤ span T.

Русский

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

LaTeX

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

Lean4

@[gcongr]
theorem span_le_span {s t : Set (ℙ K V)} (hst : s ⊆ t) : span s ≤ span t :=
  monotone_span hst

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

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

Разделы

Аффилиация

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