image_emetric_closedBall — Mathlib

English

image of a closed EMetric ball is the closed EMetric ball around the image point.

Русский

образ замкнутого шара EMetric равен замкнутому шару вокруг образа точки

LaTeX

$$$\mathrm{image}(h)(\mathrm{EMetric}.\mathrm{closedBall}(x,r)) = \mathrm{EMetric}.\mathrm{closedBall}(h(x), r)$$$

Lean4

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

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