span_le_subspace_iff

Mathlib.LinearAlgebra.Projectivization.Subspace

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

← MathLib Explorer

English

If S ⊆ W and W ≤ span S, then span S = W.

Русский

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

LaTeX

$$$S \subseteq W \wedge W \le \operatorname{span}(S) \Rightarrow \operatorname{span}(S) = W$$$

Lean4

/-- The span of a set of points is contained in a subspace if and only if the set of points is
contained in the subspace. -/
theorem span_le_subspace_iff {S : Set (ℙ K V)} {W : Subspace K V} : span S ≤ W ↔ S ⊆ W :=
  gi.gc S W

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

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

Разделы

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

Аффилиация

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