preimage_mul_right_ball — Mathlib

English

For any a ∈ G, b ∈ G, r ≥ 0, the preimage of ball around b under the map y ↦ y • a is the ball around b / a: (· * a)^{-1} ball(b,r) = ball(b / a, r).

Русский

Для любых a,b ∈ G и r: предобраз шарa вокруг b по отображению y ↦ y • a равен шар(b / a, r).

LaTeX

$$$(\cdot \;a)^{-1}\!\left(\mathrm{ball}(b,r)\right) = \mathrm{ball}(\tfrac{b}{a}, r)$$$

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_right_ball [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) :
    (fun x => x * a) ⁻¹' ball b r = ball (b / a) r :=
  by
  rw [div_eq_mul_inv]
  exact preimage_smul_ball (MulOpposite.op a) b r

Похожие утверждения