inv — Mathlib

English

Inversion x ↦ x^{-1} defines an isometry on G; i.e., edist(a^{-1}, b^{-1}) = edist(a,b) for all a,b ∈ G.

Русский

Инверсия x ↦ x^{-1} определяет изометрию на G; т.е. edist(a^{-1}, b^{-1}) = edist(a,b) для всех a,b.

LaTeX

$$$\mathrm{edist}(a^{-1}, b^{-1}) = \mathrm{edist}(a,b)$$$

Lean4

/-- Inversion `x ↦ x⁻¹` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) /-- Negation `x ↦ -x` as an `IsometryEquiv`. -/
    ]
def inv : G ≃ᵢ G where
  toEquiv := Equiv.inv G
  isometry_toFun := edist_inv_inv

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