English
In ℤ with the metric induced from ℝ, the open ball around x of radius r equals the set of integers n with floor(x − r) < n < ceil(x + r).
Русский
В \mathbb{Z} с метрикой, порожденной из \mathbb{R}, открытая окрестность вокруг x радиуса r равна множеству целых чисел n такие, что floor(x − r) < n < ceil(x + r).
LaTeX
$$$\operatorname{ball}_{\mathbb{Z}}(x,r)=\mathrm{Ioo}(\lfloor x-r\rfloor,\lceil x+r\rceil)$$$
Lean4
theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ := by
rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]