dist_inv_inv — Mathlib

English

In a group G with a metric making left and right multiplications isometries, inversion is an isometry: dist(a^{-1}, b^{-1}) = dist(a,b).

Русский

В группе G с метрикой, сохраняющей расстояния под умножением слева и справа, инверсия является изометрией: d(a^{-1}, b^{-1}) = d(a,b).

LaTeX

$$$\operatorname{dist}(a^{-1}, b^{-1}) = \operatorname{dist}(a,b)$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_inv_inv [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) :
    dist a⁻¹ b⁻¹ = dist a b :=
  (IsometryEquiv.inv G).dist_eq a b

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