English
The metric on ℤ is the restriction of the usual metric from ℝ; the preimage under the inclusion map of a real ball around x equals the intrinsic ball in ℤ around x of radius r.
Русский
Метрика на \mathbb{Z} является ограничением обычной метрики из \mathbb{R}; прообраз шара в \mathbb{R} вокруг точки x под включением равен шару в \mathbb{Z} с радиусом r.
LaTeX
$$$(\uparrow)^{-1} B_{\mathbb{R}}(x,r)=B_{\mathbb{Z}}(x,r)$$$
Lean4
theorem preimage_ball (x : ℤ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r :=
rfl