map_smul

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.map_smul

English

The diameter of the range of an isometry equals the diameter of the ambient space.

Русский

Диаметр образа изометрии равен диаметру пространства.

LaTeX

$$$\operatorname{diam}(\operatorname{range}(f)) = \operatorname{diam}(\mathrm{univ})$$$

Lean4

protected theorem map_smul [Module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) : f (c • x) = c • f x :=
  f.toLinearMap.map_smul c x

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

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

Разделы

Аффилиация

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