map_smulₛₗ

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The norm is preserved under a semilinear isometry: ||f x|| = ||x||.

Русский

Норма сохраняется под семилинейной изометрией: \|f x\| = \|x\|.

LaTeX

$$$\|f x\| = \|x\|$$$

Lean4

protected theorem map_smulₛₗ (c : R) (x : E) : f (c • x) = σ₁₂ c • f x :=
  f.toLinearMap.map_smulₛₗ c x

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

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

Разделы

Аффилиация

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