monotone_span

Mathlib.LinearAlgebra.Projectivization.Subspace

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

← MathLib Explorer

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

/-- If a set of points is a subset of another set of points, then its span will be contained in the
span of that set. -/
@[mono]
theorem monotone_span : Monotone (span : Set (ℙ K V) → Subspace K V) :=
  gi.gc.monotone_l

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

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

Разделы

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

Аффилиация

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