image_sphere — Mathlib

English

The image of a sphere under an isometry is a sphere with the image point as center.

Русский

Образ сферы под изометрией — сфера с изображенным центром.

LaTeX

$$$ h''\operatorname{Sphere}(x,r) = \operatorname{Sphere}(h(x), r) $$$

Lean4

@[simp]
theorem image_sphere (h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.sphere x r = Metric.sphere (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]

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