English
For any c ∈ G, x ∈ X, r, the preimage of a closed ball under the map y ↦ c • y is the closed ball around c^{-1} • x with radius r: (c • -)^{-1} closedBall(x,r) = closedBall(c^{-1} • x, r).
Русский
Для любого c ∈ G, x ∈ X, r: предобраз закрытого шара по отображению y ↦ c • y равен закрытому шару вокруг c^{-1} • x с радиусом r.
LaTeX
$$$(c\cdot -)^{-1}\!\left(\mathrm{closedBall}(x,r)\right) = \mathrm{closedBall}(c^{-1}\cdot x, r)$$$
Lean4
@[to_additive (attr := simp)]
theorem preimage_smul_closedBall (c : G) (x : X) (r : ℝ≥0∞) : (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r := by
rw [preimage_smul, smul_closedBall]