preimage_smul_ball — Mathlib

English

For any c ∈ G, x ∈ X, r, the preimage of ball around x with respect to the map y ↦ c • y is the ball around c^{-1} • x with the same radius: (c • -)^{-1} ball(x,r) = ball(c^{-1} • x, r).

Русский

Для любого c ∈ G, x ∈ X, r: предобраз ball(x,r) по отображению y ↦ c • y равен ball(c^{-1} • x, r).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem preimage_smul_ball (c : G) (x : X) (r : ℝ≥0∞) : (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r := by
  rw [preimage_smul, smul_ball]

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