isometry_mul_right

Mathlib.Topology.MetricSpace.IsometricSMul

URI: https://scilib.ai/kg/mathlib#isometry_mul_right

← MathLib Explorer

English

Right multiplication by a fixed element a is an isometry of the ambient metric space.

Русский

Правое умножение на фиксированное a является изометрией пространства.

LaTeX

$$$\text{Isometry }(x\mapsto x\cdot a)$$$

Lean4

@[to_additive]
theorem isometry_mul_right [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a : M) : Isometry fun x => x * a :=
  isometry_smul M (MulOpposite.op a)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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