closedBall_eq_Icc — Mathlib

English

For any real numbers x and r, the closed ball of radius r around x coincides with the closed interval [x−r, x+r].

Русский

Для любых действительных x и r замкнутая окрестность шаром радиуса r вокруг x совпадает с замкнутым интервалом [x−r, x+r].

LaTeX

$$$\operatorname{closedBall}(x,r) = [x-r,\; x+r]$$$

Lean4

theorem closedBall_eq_Icc {x r : ℝ} : closedBall x r = Icc (x - r) (x + r) :=
  by
  ext y
  rw [mem_closedBall, dist_comm, Real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add', sub_le_comm]

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