isIsIsometricVAdd — Mathlib

English

If M acts on X by isometries, then it also acts by isometries on the additive space Additive M via the addition action.

Русский

Если M действует на X изометрично, то над множеством Additive M получаем изометрию через операцию сложения.

LaTeX

$$$\\forall c \\in M, \\forall x,y \\in X:\\ edist(c + x, c + y) = edist(x,y).$$$

Lean4

instance isIsIsometricVAdd : IsIsometricVAdd (Additive M) X :=
  ⟨fun c => isometry_smul X c.toMul⟩

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