edist_inv_inv — Mathlib

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]

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