lean_workbook_plus_21611
ProvedThe function for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21611 (x : ℝ) (hx: x ≥ 0) : (1 / (1 + x ^ 2)) ≥ 1 - x / 2 := by sorry
Source
The function for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_21611 (x : ℝ) (hx: x ≥ 0) : (1 / (1 + x ^ 2)) ≥ 1 - x / 2 := by sorry