English
Let G be a group with a pseudo-extended metric and let G act on itself by left multiplication by isometries. Then for all a, b, c in G, the left translation by a preserves the edistance: edist(a/b, a/c) = edist(b, c). In particular, left multiplication by any a is an isometry of G.
Русский
Пусть G — группа с псевдо-расстоянием (edist) и действует на себе по левому умножению, причём действие является изометрическим. Тогда для любых a, b, c ∈ G левое перенесение на a сохраняет edist: edist(a/b, a/c) = edist(b, c). В частности, левое умножение на произвольный a — это изометрия на G.
LaTeX
$$$\mathrm{edist}(a/b, a/c) = \mathrm{edist}(b,c)$$$
Lean4
@[to_additive (attr := simp)]
theorem edist_div_left [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) :
edist (a / b) (a / c) = edist b c := by rw [div_eq_mul_inv, div_eq_mul_inv, edist_mul_left, edist_inv_inv]
