dist_div_right — Mathlib

English

In a metric setting with a DivInvMonoid M and an isometric right action, right-division by c preserves distances: dist(a/c, b/c) = dist(a,b).

Русский

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

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