nndist_mul_right — Mathlib

English

Let M be a metric space with a right isometric action by M. Then for all a,b,c ∈ M, the nonnegative distance is preserved under right-multiplication by c: nndist(a c, b c) = nndist(a,b).

Русский

Пусть M — метрическое пространство с правым изометрическим действием M. Тогда для всех a,b,c ∈ M сохраняется ненегативное расстояние под правым умножением на c: nndist(a c, b c) = nndist(a,b).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem nndist_mul_right [PseudoMetricSpace M] [Mul M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) :
    nndist (a * c) (b * c) = nndist a b :=
  nndist_smul (MulOpposite.op c) a b

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