lean_workbook_plus_35072
ProvedGiven , find the values of and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35072 (f : ℝ → ℝ) (hf : ∀ x, f (f x) = 1 - x^2) : f 1 = 0 ∧ f 0 = 1 := by sorry
Source
Given , find the values of and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35072 (f : ℝ → ℝ) (hf : ∀ x, f (f x) = 1 - x^2) : f 1 = 0 ∧ f 0 = 1 := by sorry