lean_workbook_plus_33041

Proved

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

For $1.4<x<1.6$ and $k\in\mathbb{N}, k\ge3$ , holds the equality $\left\lfloor x+\dfrac{1}{k}\right\rfloor=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33041 (x : ℝ) (k : ℕ) (h₁ : 1.4 < x ∧ x < 1.6) (h₂ : 3 ≤ k) : ⌊x + 1 / k⌋ = 1   :=  by sorry

Source