preimage_emetric_closedBall — Mathlib

English

If f is an isometry, then for every x and r, the preimage of the closed ball around f(x) with radius r is exactly the closed ball around x with radius r.

Русский

Если f — изометрия, то для любого x и r прообраз замкнутого шара вокруг f(x) радиуса r равен замкнутому шару вокруг x радиуса r.

LaTeX

$$$Isometry(f) \rightarrow \forall x\,\forall r:\, f^{-1}(\mathrm{Metric.closedBall}(f(x),r)) = \mathrm{Metric.closedBall}(x,r)$$$

Lean4

theorem preimage_emetric_closedBall (h : Isometry f) (x : α) (r : ℝ≥0∞) :
    f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r :=
  by
  ext y
  simp [h.edist_eq]

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