lean_workbook_plus_27457
ProvedIf for all , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27457 (x y : ℝ) (h : ∀ e : ℝ, e > 0 → x + e < y) : x ≤ y := by sorry
Source
If for all , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27457 (x y : ℝ) (h : ∀ e : ℝ, e > 0 → x + e < y) : x ≤ y := by sorry