dist_smul — Mathlib

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

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