lean_workbook_plus_48648

Proved

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

For $n = a + k$ , where $a = \lfloor n \rfloor$ and $0 < k < 1$ , prove that $\lfloor n \rfloor + 1 = \lceil n \rceil$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48648 (n a k : ℝ) (h₁ : n = a + k) (h₂ : a = ⌊n⌋) (h₃ : 0 < k) (h₄ : k < 1) : ⌊n⌋ + 1 = ⌈n⌉   :=  by sorry

Source