English
For any c ∈ G, the image of a closed ball under the action by c is the closed ball around c • x with the same radius: c • closedBall(x,r) = closedBall(c • x, r).
Русский
Для любого c ∈ G образ закрытого шара под действием c — это закрытый шар вокруг c • x с тем же радиусом.
LaTeX
$$$c\cdot \overline{\mathrm{Ball}}(x,r) = \overline{\mathrm{Ball}}(c\cdot x, r)$$$
Lean4
@[to_additive (attr := simp)]
theorem smul_closedBall (c : G) (x : X) (r : ℝ≥0∞) : c • closedBall x r = closedBall (c • x) r :=
(IsometryEquiv.constSMul c).image_emetric_closedBall _ _