lean_workbook_plus_75403

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $a$ and $b$ be two real numbers such that $a\le b$ . Prove that $\bigcap_{n\in N^{*}}[a-\frac{1}{n},b+\frac{1}{n}]=[a,b]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75403 (a b : ℝ) (h : a ≤ b) :
  ⋂ (n : ℕ), (Set.Icc (a - 1 / n) (b + 1 / n)) = Set.Icc a b   :=  by sorry

Source