English
The closed ball in ℕ around x with radius r equals the integer interval [ceil(x−r), floor(x+r)]. More precisely, closedBallℕ(x,r) = Icc(ceil(x−r), floor(x+r)).
Русский
Замкнутый шар в ℕ вокруг x радиуса r равен целочисленному интервалу [ceil(x−r), floor(x+r)].
LaTeX
$$$\operatorname{closedBall}_{\mathbb{N}}(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
rcases le_or_gt 0 r with (hr | hr)
· rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
positivity
· rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
calc
⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
_ < ⌈↑x - r⌉₊ := by
rw [floor_natCast, Nat.lt_ceil]
linarith
