smul_sphere — Mathlib

English

Under an isometric action, the image of a sphere is the sphere centered at the translated point with the same radius: c • sphere(x,r) = sphere(c • x, r).

Русский

При изометрическом действии образ сферы — сфера с тем же радиусом и центром, смещённым на действие: c•sphere(x,r) = sphere(c•x, r).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem smul_sphere (c : G) (x : X) (r : ℝ) : c • sphere x r = sphere (c • x) r :=
  (IsometryEquiv.constSMul c).image_sphere _ _

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