lean_workbook_plus_36894
Provedwith equality iff
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36894 (x : ℝ) : x / (1 + x ^ 2) ≤ 1 / 2 ∧ (x = 1 ↔ x / (1 + x ^ 2) = 1 / 2) := by sorry
Source
with equality iff
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_36894 (x : ℝ) : x / (1 + x ^ 2) ≤ 1 / 2 ∧ (x = 1 ↔ x / (1 + x ^ 2) = 1 / 2) := by sorry