ball_eq_Ioo — Mathlib

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]

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