lean_workbook_plus_41163
ProvedUse the inequality for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_41163 : ∀ t : ℝ, t ≤ 1 → 1 / (1 + t ^ 2) ≤ 27 * (2 - t) / 50 := by sorry
Source
Use the inequality for all .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_41163 : ∀ t : ℝ, t ≤ 1 → 1 / (1 + t ^ 2) ≤ 27 * (2 - t) / 50 := by sorry