preimage_emetric_ball — Mathlib

English

If f is an isometry, then for all x and r, the preimage of the EMetric.ball around f(x) with radius r equals the EMetric.ball around x with radius r.

Русский

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

LaTeX

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

Lean4

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

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