lean_workbook_plus_40069
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove that\n(a) if y=x2+1x2+x+1 , then 21≤y≤23 ,\n(b) if y=x2+x+1x2+1 , then 32≤y≤2 .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40069 (x y : ℝ) (h₁ : y = (x^2 + x + 1) / (x^2 + 1)) : 1 / 2 ≤ y ∧ y ≤ 3 / 2 := by sorry
View graph