preimage_ball — Mathlib

English

For a linear isometry e and any x in E₂, the preimage of the sphere of radius r around x equals the sphere of radius r around e^{-1} x.

Русский

Для линейной изометрии e предобраз сферы радиуса r вокруг x равен сфере радиуса r вокруг e^{-1} x.

LaTeX

$$$e^{-1}'\,\mathsf{Sphere}(x,r) = \mathsf{Sphere}(e^{-1} x, r)$$$

Lean4

@[simp]
theorem preimage_ball (x : E₂) (r : ℝ) : e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r :=
  e.toIsometryEquiv.preimage_ball x r

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