preimage_closedBall — Mathlib

English

The image of a closed ball under a linear isometry is the closed ball of the same radius around the image of the center.

Русский

Образ замкнутого шара линейной изометрией — замкнутый шар той же радиуса вокруг образа центра.

LaTeX

$$$e''\,\mathsf{ClosedBall}(x,r) = \mathsf{ClosedBall}(e x, r)$$$

Lean4

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

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