English
If a group M acts on a pseudo-emetric space X by isometries, then the induced action on ULift X, defined by c ⋅ ULift x = ULift (c ⋅ x), is again isometric in the sense that for all c ∈ M and x, y ∈ X, edist(c ⋅ ULift x, c ⋅ ULift y) = edist(ULift x, ULift y).
Русский
Если множество M действует на псевдо-эмитрическом пространстве X изометрично, то индуцированное действие на ULift X, заданное как c ⋅ ULift x = ULift (c ⋅ x), также изометрично: для всех c ∈ M и x, y ∈ X выполняется edist(c ⋅ ULift x, c ⋅ ULift y) = edist(ULift x, ULift y).
LaTeX
$$$\\forall c \\in M\\, \\forall x,y \\in X:\\ edist\\big(c \\cdot \\mathrm{ULift}(x),\, c \\cdot \\mathrm{ULift}(y)\\big) = edist\\big(\\mathrm{ULift}(x), \\mathrm{ULift}(y)\\big).$$$
Lean4
@[to_additive]
instance isIsometricSMul' : IsIsometricSMul M (ULift X) :=
⟨fun c x y => by simpa only using edist_smul_left c x.1 y.1⟩
