lean_workbook_plus_11657
ProvedThe solution to the inequality is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11657 (c : ℝ) : -3 * (c + 1) * (c - 13/3) ≥ 0 ↔ -1 ≤ c ∧ c ≤ 13/3 := by sorry
Source
The solution to the inequality is .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11657 (c : ℝ) : -3 * (c + 1) * (c - 13/3) ≥ 0 ↔ -1 ≤ c ∧ c ≤ 13/3 := by sorry