edist_smul_left — Mathlib

English

In a pseudo-metric space with an isometric SMul action, the left action preserves edistance: edist(c•x, c•y) = edist(x,y).

Русский

При изометрическом действии действует сохранение eddist слева: edist(c•x, c•y) = edist(x,y).

LaTeX

$$$\forall c\in M,\ \forall x,y:\; \mathrm{edist}(c\cdot x, c\cdot y) = \mathrm{edist}(x,y)$$$

Lean4

@[to_additive (attr := simp)]
theorem edist_smul_left [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : edist (c • x) (c • y) = edist x y :=
  isometry_smul X c x y

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