lean_workbook_plus_57045
Proved<->
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57045 (x : ℝ) : x * (x - 4) ≤ 0 ↔ 0 ≤ x ∧ x ≤ 4 := by sorry
Source
<->
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_57045 (x : ℝ) : x * (x - 4) ≤ 0 ↔ 0 ≤ x ∧ x ≤ 4 := by sorry