dist_mul_left — Mathlib

English

In a metric space M where M acts on itself by left multiplication by a, the distance satisfies dist(a b, a c) = dist(b, c) for all a,b,c ∈ M.

Русский

В метрическом пространстве M, где M действует на себе по левому умножению на a, выполняется dist(a b, a c) = dist(b, c) для всех a,b,c ∈ M.

LaTeX

$$$\operatorname{dist}(a b, a c) = \operatorname{dist}(b, c)$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_mul_left [PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) :
    dist (a * b) (a * c) = dist b c :=
  dist_smul a b c

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