lean_workbook_plus_44180
ProvedConsider the cases: 1) , 2) , 3) .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44180 (a : ℝ) : a / 2 < 0 ∨ 0 ≤ a / 2 ∧ a / 2 ≤ 2 ∨ a / 2 > 2 := by sorry
Source
Consider the cases: 1) , 2) , 3) .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_44180 (a : ℝ) : a / 2 < 0 ∨ 0 ≤ a / 2 ∧ a / 2 ≤ 2 ∨ a / 2 > 2 := by sorry