isIsometricSMul — Mathlib

English

If M acts isometrically on a metric space X, then the ULift of M acts isometrically on X as well; distance is preserved under the action of any element of ULift M.

Русский

Если M действует изометрично на X, то ULift M действует изометрически на X; расстояние сохраняется под действием любого элемента ULift M.

LaTeX

$$$\forall c\in \mathrm{ULift}(M),\; d(c\cdot x, c\cdot y) = d(x,y)\quad\text{for all }x,y\in X$$$

Lean4

@[to_additive]
instance isIsometricSMul : IsIsometricSMul (ULift M) X :=
  ⟨fun c => by simpa only using isometry_smul X c.down⟩

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