preimage_smul_ball — Mathlib

English

The preimage of a ball under the smul action by c is the ball around c^{-1}•x of the same radius: (c•·)^{-1} Ball(x,r) = Ball(c^{-1}•x, r).

Русский

Образ-функции под действием c: предобразBall(x,r) равен Ball(c^{-1}•x, r).

LaTeX

$$$ (c \cdot)^{-1} \mathrm{Ball}(x,r) = \mathrm{Ball}(c^{-1}\cdot x, r) $$$

Lean4

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

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