dist_mul_right — Mathlib

English

Let M be a metric space with a right action by M given by multiplication that preserves distances. Then for all a,b,c in M, the distance between a and b is unchanged after right-multiplying by c:

Русский

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

LaTeX

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

Lean4

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

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