lean_workbook_plus_66075
ProvedWe need and so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66075 : ∀ y : ℝ, (y ≤ -1 ∨ 0 ≤ y ∧ y ≤ 1) ↔ 2*y - 2*y^3 ≥ 0 := by sorry
Source
We need and so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_66075 : ∀ y : ℝ, (y ≤ -1 ∨ 0 ≤ y ∧ y ≤ 1) ↔ 2*y - 2*y^3 ≥ 0 := by sorry