lean_workbook_plus_32321

Proved

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

or $\lfloor a\rfloor <\lfloor b\rfloor\implies a\leq b$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32321 (a b : ℝ) (h : ⌊a⌋ < ⌊b⌋) : a ≤ b   :=  by sorry

Source