Solving a strict quadratic inequality

Proved

WorkbookSource.problem_19386

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Given the inequality $2x^2 + x - 6 < 0$ , find the set of $x$ -values that satisfy it.

Source: InternLM Lean-Workbook, record lean_workbook_19386 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_19386 (x : ℝ) : 2 * x ^ 2 + x - 6 < 0 ↔ -2 < x ∧ x < 3/2  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_19386; Apache-2.0

View graph