map_smul

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The distance is preserved by a linear isometry: dist(e x, e y) = dist(x, y).

Русский

Изометрия сохраняет евклидово расстояние: dist(e x, e y) = dist(x, y).

LaTeX

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

Lean4

theorem map_smul [Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) : e (c • x) = c • e x :=
  e.1.map_smul c x

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

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

Разделы

Аффилиация

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