lean_workbook_plus_81212

Proved

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

Let $x$ , $y$ be real numbers. Show that $x \leq y+\epsilon$ for all real numbers $\epsilon >0$ (for every $\epsilon>0)$ if and only if $x \leq y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81212 (x y : ℝ) (h : ∀ ε : ℝ, ε > 0 → x ≤ y + ε) : x ≤ y   :=  by sorry

Source