lean_workbook_plus_66532
Proved(x - 1)(x - 3) 0 x ( - ,1] [3, )
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66532 (x : ℝ) (hx: (x - 1) * (x - 3) ≥ 0) : x ≤ 1 ∨ x ≥ 3 := by sorry
Source
(x - 1)(x - 3) 0 x ( - ,1] [3, )
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_66532 (x : ℝ) (hx: (x - 1) * (x - 3) ≥ 0) : x ≤ 1 ∨ x ≥ 3 := by sorry