preimage_mul_left_ball — Mathlib

English

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

Русский

Для любых a,b ∈ G и r ∈ ℝ≥0∞ предобраз шарa вокруг b по отображению y ↦ a • y равен шар(a^{-1} • b, r).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_left_ball [IsIsometricSMul G G] (a b : G) (r : ℝ≥0∞) : (a * ·) ⁻¹' ball b r = ball (a⁻¹ * b) r :=
  preimage_smul_ball a b r

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