edist_div_right — Mathlib

English

Division by a fixed element preserves edistance: edist(a/c, b/c) = edist(a,b).

Русский

Деление на фиксированный элемент сохраняет edрасстояние: edist(a/c, b/c) = edist(a,b).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem edist_div_right [DivInvMonoid M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) :
    edist (a / c) (b / c) = edist a b := by simp only [div_eq_mul_inv, edist_mul_right]

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