Icc_eq_closedBall — Mathlib

English

For real numbers x ≤ y, the closed interval [x,y] equals the closed ball with center (x+y)/2 and radius (y−x)/2.

Русский

Для действительных x ≤ y замкнутый интервал [x,y] равен замкнутой сфере с центром в \frac{x+y}{2} и радиусом \frac{y-x}{2}.

LaTeX

$$$Icc(x,y) = \operatorname{closedBall}\left(\frac{x+y}{2}, \frac{y-x}{2}\right)$$$

Lean4

theorem Icc_eq_closedBall (x y : ℝ) : Icc x y = closedBall ((x + y) / 2) ((y - x) / 2) := by
  rw [Real.closedBall_eq_Icc, ← 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]

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