ball_eq_openSegment — Mathlib

English

For a real r and ε ≥ 0, the closed ball centered at r with radius ε equals the segment between r−ε and r+ε.

Русский

Для действительного числа r и ε ≥ 0, замкнутый шар с центром r и радиусом ε равен отрезку между r−ε и r+ε.

LaTeX

$$$$ \mathrm{closedBall}(r,\epsilon) = \mathrm{segment}_{\mathbb{R}}(r-\epsilon, r+\epsilon) \text{ for } \epsilon \ge 0. $$$$

Lean4

theorem ball_eq_openSegment (hε : 0 < ε) : ball r ε = openSegment ℝ (r - ε) (r + ε) := by
  rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]

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