Ioo_eq_ball — Mathlib

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]

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