ball_eq_Ioo — Mathlib

English

In the real line, the metric ball equals the open interval: ball x r = (x−r, x+r).

Русский

В действительной линии метрический шар равен открытому интервалу: ball x r = (x−r, x+r).

LaTeX

$$$\\text{ball}(x,r)=\\mathrm{Ioo}(x-r,\,x+r)$ for all real x,r.$$

Lean4

theorem ball_eq_Ioo (x r : ℝ) : ball x r = Ioo (x - r) (x + r) :=
  Set.ext fun y => by rw [mem_ball, dist_comm, Real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add', sub_lt_comm]

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