preimage_ball — Mathlib

English

The preimage of a closed ball under a linear isometry is a closed ball of the same radius.

Русский

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

LaTeX

$$Set.preimage (f) (ClosedBall(f(x), r)) = ClosedBall(x, r)$$

Lean4

@[simp]
theorem preimage_ball (x : E) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r :=
  f.isometry.preimage_ball x r

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