nndist_mul_left — Mathlib

English

In a metric space M with a left action by M that is isometric, the nonnegative distance is preserved under left multiplication: nndist(a b, a c) = nndist(b, c) for all a,b,c.

Русский

В метрическом пространстве M с изометрическим левым действием сохраняется nndist: nndist(a b, a c) = nndist(b, c).

LaTeX

$$$\mathrm{nndist}(a b, a c) = \mathrm{nndist}(b, c)$$$

Lean4

@[to_additive (attr := simp)]
theorem nndist_mul_left [PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) :
    nndist (a * b) (a * c) = nndist b c :=
  nndist_smul a b c

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