lean_workbook_plus_23062

Proved

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

Let $y=x-\frac 12$ and the equation is $\lfloor y+1\rfloor+\lfloor y\rfloor=\lfloor 2y+1\rfloor$ $\iff$ $2\lfloor y\rfloor=\lfloor 2y\rfloor$ $\iff$ $y\in[n,n+\frac 12)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23062  (y : ℝ)
  (n : ℤ)
  (h₀ : n ≤ y)
  (h₁ : y < n + 1 / 2) :
  Int.floor (y + 1) + Int.floor y = Int.floor (2 * y + 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph