Real_Numbers_Between_Epsilons
Provedproofwikireal-analysis
If for all ε > 0 we have a - ε < b < a + ε, then a = b.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Real_Numbers_Between_Epsilons (a b : ℝ) (h : ∀ ε : ℝ, ε > 0 → a - ε < b ∧ b < a + ε) : a = b := by sorry
Source