preimage_smul_closedBall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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