image_emetric_ball — Mathlib

English

image of an EMetric ball under h equals the EMetric ball around the image point.

Русский

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

LaTeX

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

Lean4

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

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