lean_workbook_plus_58837
ProvedSince , for all , either or .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58837 (f : ℝ → ℝ) (hx: ∀ x, (f x)^2 = 4) : ∀ x, (f x = 2 ∨ f x = -2) := by sorry
Source
Since , for all , either or .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_58837 (f : ℝ → ℝ) (hx: ∀ x, (f x)^2 = 4) : ∀ x, (f x = 2 ∨ f x = -2) := by sorry