lean_workbook_plus_55638

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Sketch the graph of $y = 3p^3 + 3p^2 - 3p$ and find its range for $-2 \leq p \leq \frac{2}{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55638 (p : ℝ) (hp : -2 ≤ p ∧ p ≤ 2/3) : -6 ≤ 3 * p ^ 3 + 3 * p ^ 2 - 3 * p ∧ 3 * p ^ 3 + 3 * p ^ 2 - 3 * p ≤ 6   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph