English
Under an isometric action, the image of a sphere is the sphere centered at the translated point with the same radius: c • sphere(x,r) = sphere(c • x, r).
Русский
При изометрическом действии образ сферы — сфера с тем же радиусом и центром, смещённым на действие: c•sphere(x,r) = sphere(c•x, r).
LaTeX
$$$ c \cdot \mathrm{sphere}(x, r) = \mathrm{sphere}(c\cdot x, r) $$$
Lean4
@[to_additive (attr := simp)]
theorem smul_sphere (c : G) (x : X) (r : ℝ) : c • sphere x r = sphere (c • x) r :=
(IsometryEquiv.constSMul c).image_sphere _ _