vectorSpan_singleton

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#vectorSpan_singleton

← MathLib Explorer

English

The vectorSpan of a single point is the zero subspace ⊥.

Русский

VectorSpan одиночного элемента равен нулевому подпространству ⊥.

LaTeX

$$$ \\operatorname{vectorSpan} \\ k\\ {p} = (\\bot : Submodule k V) $$$

Lean4

/-- The `vectorSpan` of a single point is `⊥`. -/
@[simp]
theorem vectorSpan_singleton (p : P) : vectorSpan k ({ p } : Set P) = ⊥ := by simp [vectorSpan_def]

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

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

Разделы

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

Аффилиация

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