English
In a group with a compatible isometric SMul, edist(a⁻¹ b⁻¹) = edist(a,b).
Русский
В группе с совместимым изометрическим SMul: edist(a⁻¹ b⁻¹) = edist(a,b).
LaTeX
$$$\mathrm{edist}(a^{-1}, b^{-1}) = \mathrm{edist}(a,b)$$$
Lean4
@[to_additive (attr := simp)]
theorem edist_inv_inv [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) :
edist a⁻¹ b⁻¹ = edist a b := by
rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_inv_cancel, one_mul, inv_mul_cancel_right, edist_comm]