English
For any a ∈ G, b ∈ G, r ≥ 0, the preimage of closedBall around b under the map y ↦ y • a is the closedBall around b / a: (· * a)^{-1} closedBall(b,r) = closedBall(b / a, r).
Русский
Для любых a,b ∈ G и r: предобраз закрытого шара по отображению y ↦ y • a равен closedBall(b/a, r).
LaTeX
$$$(\cdot \;a)^{-1}\!\left(\mathrm{closedBall}(b,r)\right) = \mathrm{closedBall}(b/a, r)$$$
Lean4
@[to_additive (attr := simp)]
theorem preimage_mul_right_closedBall [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) :
(fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r :=
by
rw [div_eq_mul_inv]
exact preimage_smul_closedBall (MulOpposite.op a) b r