English
If a group G acts on a metric space X by isometries, then for any fixed c ∈ G the map x ↦ c • x is an isometry of X; equivalently, for all x, y ∈ X, dist(c • x, c • y) = dist(x, y).
Русский
Пусть G действует на метрическом пространстве X по изометриям. Для фиксированного c ∈ G отображение x ↦ c • x является изометрией X; то есть для всех x, y ∈ X выполняется dist(c • x, c • y) = dist(x, y).
LaTeX
$$$\operatorname{dist}(c\cdot x, c\cdot y) = \operatorname{dist}(x,y)$$$
Lean4
/-- If a group `G` acts on `X` by isometries, then `IsometryEquiv.constSMul` is the isometry of
`X` given by multiplication of a constant element of the group. -/
@[to_additive (attr := simps! toEquiv apply) /-- If an additive group `G` acts on `X` by isometries,
then `IsometryEquiv.constVAdd` is the isometry of `X` given by addition of a constant element of the
group. -/
]
def constSMul (c : G) : X ≃ᵢ X where
toEquiv := MulAction.toPerm c
isometry_toFun := isometry_smul X c
