lean_workbook_plus_56740
Proved, so .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56740 (x : ℝ) : (5*x-6-x^2)/2 ≥ 0 ↔ 2 ≤ x ∧ x ≤ 3 := by sorry
Source
, so .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_56740 (x : ℝ) : (5*x-6-x^2)/2 ≥ 0 ↔ 2 ≤ x ∧ x ≤ 3 := by sorry