closedBall_eq_Icc — Mathlib

English

In ℤ, the closed ball around x with radius r is the integer interval [ceil(x−r), floor(x+r)].

Русский

В \mathbb{Z} замкнутая окрестность вокруг x радиуса r равна целочисленному интервалу [ceil(x−r), floor(x+r)].

LaTeX

$$$\operatorname{closedBall}_{\mathbb{Z}}(x,r)=\mathrm{Icc}(\lceil x-r\rceil,\lfloor x+r\rfloor)$$$

Lean4

theorem closedBall_eq_Icc (x : ℤ) (r : ℝ) : closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ := by
  rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

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