preimage_mul_left_closedBall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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