English
In the real line, the open interval (x, y) equals the open ball centered at (x+y)/2 with radius (y−x)/2.
Русский
На действительной прямой открытый промежуток (x, y) равен открытой шаре с центром в \frac{x+y}{2} и радиусом \frac{y-x}{2}.
LaTeX
$$$Ioo(x,y) = \mathrm{ball}\left(\frac{x+y}{2}, \frac{y-x}{2}\right)$$$
Lean4
theorem Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2) := by
rw [Real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two, ← add_div, add_assoc,
add_sub_cancel, add_self_div_two]