preimage_mul_right_closedBall — Mathlib

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

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