lean_workbook_plus_63307

Proved

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

If $f(x) = \lfloor x \rfloor +1$ then $f(f(x)) = f( \lfloor x \rfloor +1 ) = \lfloor \lfloor x \rfloor +1 \rfloor + 1 = \lfloor x \rfloor + 2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63307  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = Int.floor x + 1) :
  ∀ x, f (f x) = Int.floor x + 2   :=  by sorry

Source