lean_workbook_plus_75499

Proved

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

Let positive integer $n>9$ We easily check that : a) $5<\\frac {n-9}{\\sqrt 2}+5<\\frac {n-1}{\\sqrt 2}<\\frac {n-8}{\\sqrt 2}+5<\\frac n{\\sqrt 2}$ b) $\\frac {n-9}{\\sqrt 2}+5<\\frac n{\\sqrt 2}-1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75499 (n : ℕ) (hn : 9 < n) : ((n-9) / Real.sqrt 2 + 5 < (n-1) / Real.sqrt 2 ∧ (n-1) / Real.sqrt 2 < (n-8) / Real.sqrt 2 + 5 ∧ (n-8) / Real.sqrt 2 + 5 < n / Real.sqrt 2 ) ∧ ((n-9) / Real.sqrt 2 + 5 < n / Real.sqrt 2 - 1)   :=  by sorry

Source

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

View graph