divRight — Mathlib

English

For any c ∈ G, the map y ↦ y / c is an isometry of G; equivalently, edist(a/c, b/c) = edist(a,b) for all a,b ∈ G.

Русский

Для любого c ∈ G отображение y ↦ y / c является изометрией на G; то есть edist(a/c, b/c) = edist(a,b) для всех a,b ∈ G.

LaTeX

$$$\mathrm{edist}(a/c, b/c) = \mathrm{edist}(a,b)$$$

Lean4

/-- Division `y ↦ y / x` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) /-- Subtraction `y ↦ y - x` as an `IsometryEquiv`. -/
    ]
def divRight [IsIsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G
    where
  toEquiv := Equiv.divRight c
  isometry_toFun a b := edist_div_right a b c

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