nndist_smul — Mathlib

English

If M acts on a metric space X by isometries, then the induced nonnegative distance nndist is preserved under the action: nndist(c•x, c•y) = nndist(x,y).

Русский

Если M действует на метрическом пространстве X изометрически, то квадростепенная дистанция nndist сохраняется под действием: nndist(c•x, c•y) = nndist(x,y).

LaTeX

$$$\mathrm{nndist}(c\cdot x, c\cdot y) = \mathrm{nndist}(x,y)$$$

Lean4

@[to_additive (attr := simp)]
theorem nndist_smul [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) :
    nndist (c • x) (c • y) = nndist x y :=
  (isometry_smul X c).nndist_eq x y

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