map_smulₛₗ

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The edistance is preserved: edist(e x, e y) = edist(x, y).

Русский

Расстояние в эдистансах сохраняется: edist(e x, e y) = edist(x, y).

LaTeX

$$$ edist(e(x), e(y)) = edist(x, y) $$$

Lean4

theorem map_smulₛₗ (c : R) (x : E) : e (c • x) = σ₁₂ c • e x :=
  e.1.map_smulₛₗ c x

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

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

Разделы

Аффилиация

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