edist_mul_left — Mathlib

English

In a pseudo-EMetric space M with isometric SMul, for a fixed a ∈ M and x,y ∈ M, edist(a•x, a•y) = edist(x,y).

Русский

В псевдометрическом пространстве edist сохраняется при левом умножении фиксированного элемента: edist(a•x, a•y) = edist(x,y).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem edist_mul_left [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a b c : M) :
    edist (a * b) (a * c) = edist b c :=
  isometry_mul_left a b c

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