nndist_div_right — Mathlib

English

In a metric space with a right isometric action, nn-distance is preserved under right-division by c: nndist(a/c, b/c) = nndist(a,b).

Русский

В метрическом пространстве с правым изометрическим действием nn-расстояние сохраняется под правым делением на 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_div_right [DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) :
    nndist (a / c) (b / c) = nndist a b := by simp only [div_eq_mul_inv, nndist_mul_right]

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