preimage_emetric_closedBall — Mathlib

English

preimage of a closed EMetric ball equals the closed EMetric ball around the inverse image.

Русский

предобраз замкнутого шара EMetric равен замкнутому шару вокруг обратного изображения

LaTeX

$$$\mathrm{preimage}(h)(\mathrm{EMetric}.\mathrm{closedBall}(x,r)) = \mathrm{EMetric}.\mathrm{closedBall}(h^{-1}(x), r)$$$

Lean4

@[simp]
theorem preimage_emetric_closedBall (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
    h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r := by
  rw [← h.isometry.preimage_emetric_closedBall (h.symm x) r, h.apply_symm_apply]

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