lean_workbook_plus_52853

Proved

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

Since $t^2-2t+1 = (t-1)^2 \ge 0$ , we have that $2t \le 1+t^2$ , or equivalently $\dfrac{t}{1+t^2} \le \dfrac{1}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52853  (t : ℝ) :
  2 * t ≤ 1 + t^2   :=  by sorry

Source