nndist_inv_inv — Mathlib

English

In a metric group with isometric inversion, nndist(a^{-1}, b^{-1}) = nndist(a,b).

Русский

В метрической группе с изометричной инверсией nn-расстояние сохраняется при инверсии: nndist(a^{-1}, b^{-1}) = nndist(a,b).

LaTeX

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

Lean4

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

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