English
If M acts on a metric space X by isometries, then the action by c ∈ M preserves distances: dist(c•x, c•y) = dist(x,y) for all x,y ∈ X.
Русский
Если множество M действует на метрическое пространство X изометрически, то действие элементами c сохраняет расстояния: dist(c•x, c•y) = dist(x,y) для всех x,y ∈ X.
LaTeX
$$$\operatorname{dist}(c\cdot x, c\cdot y) = \operatorname{dist}(x,y)$$$
Lean4
@[to_additive (attr := simp)]
theorem dist_smul [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) :
dist (c • x) (c • y) = dist x y :=
(isometry_smul X c).dist_eq x y