lean_workbook_plus_62843

Proved

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

In general, if you have $x,y\in \mathbb{R}$ fixed such that $x+\varepsilon >y$ for all $\varepsilon >0$ , then you can conclude $x\geq y$ . With $x=a$ and $y=0$ we get $a\geq 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62843  (a : ℝ)
  (h : ∀ ε > 0, a + ε > 0) :
  a ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph