Prove2Me

lean_workbook_plus_2536

Proved

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

Then\n\n1≤x≤11⇒1≤⌊x⌋≤111 \le x \le 11 \Rightarrow 1 \le \lfloor x\rfloor \le 11

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2536 (x : ℝ) (hx : 1 ≤ x ∧ x ≤ 11) : 1 ≤ ⌊x⌋ ∧ ⌊x⌋ ≤ 11   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph