vectorSpan_def

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

English

The definition of vectorSpan is that it equals the span of s − s.

Русский

Определение vectorSpan: vectorSpan k s = span k (s − s).

LaTeX

$$$ \\operatorname{vectorSpan} \\ k\\ s = \\operatorname{Submodule}.span\\ k (s -\\!\\!\\- s) $$$

Lean4

/-- The definition of `vectorSpan`, for rewriting. -/
theorem vectorSpan_def (s : Set P) : vectorSpan k s = Submodule.span k (s -ᵥ s) :=
  rfl

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

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

Разделы

Аффилиация

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