preimage_smul_sphere — Mathlib

English

The preimage of a sphere under the smul action equals the sphere around c^{-1}•x with the same radius: (c•·)^{-1} sphere(x,r) = sphere(c^{-1}•x, r).

Русский

Предобраз сферы под действием smul равен сфере вокруг c^{-1}•x радиуса r.

LaTeX

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

Lean4

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

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