lean_workbook_plus_544
Provedand so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_544 (f : ℝ → ℝ) (h : ∀ x, f x ^ 2 = 1) : Set.range f ⊆ {1, -1} := by sorrySource
and so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_544 (f : ℝ → ℝ) (h : ∀ x, f x ^ 2 = 1) : Set.range f ⊆ {1, -1} := by sorry