isIsometricSMul — Mathlib

English

If M is a monoid acting isometrically on a metric space X, then its group of units Mˣ also acts isometrically on X by restricting the action to units.

Русский

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

LaTeX

$$$\text{IsIsometricSMul}(M^{\times}, X)$$$

Lean4

@[to_additive]
instance isIsometricSMul [Monoid M] : IsIsometricSMul Mˣ X :=
  ⟨fun c => isometry_smul X (c : M)⟩

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