lean_workbook_plus_17652
ProvedYour teacher graphed .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17652 (x : ℝ) : |x| > Real.sqrt 2 ↔ x < -Real.sqrt 2 ∨ x > Real.sqrt 2 := by sorry
Source
Your teacher graphed .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_17652 (x : ℝ) : |x| > Real.sqrt 2 ↔ x < -Real.sqrt 2 ∨ x > Real.sqrt 2 := by sorry