preimage_sphere — Mathlib

English

The preimage of a sphere by an isometry equals the sphere around the symmetric image center.

Русский

Предобраз сферы под изометрией равен сфере вокруг симметричного изображения центра.

LaTeX

$$$ h^{-1}'\!\operatorname{Sphere}(x,r) = \operatorname{Sphere}(h^{-1}(x), r) $$$

Lean4

@[simp]
theorem preimage_sphere (h : α ≃ᵢ β) (x : β) (r : ℝ) : h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r := by
  rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]

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