span_singleton_eq_range

Mathlib.LinearAlgebra.Span.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.span_singleton_eq_range

English

The range of toSpanSingleton x is the span of x.

Русский

Образ toSpanSingleton x равен спану x.

LaTeX

$$$\operatorname{range}(\operatorname{toSpanSingleton}\,R\,M\,x) = \operatorname{span} R\{x\}$$$

Lean4

theorem span_singleton_eq_range (x : M) : (R ∙ x) = range (toSpanSingleton R M x) :=
  range_toSpanSingleton x |>.symm

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

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

Разделы

Аффилиация

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