lean_workbook_plus_3415
ProvedIf , find .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3415 (f : ℝ → ℝ) (hf : ∀ x, f (f x) = 1 - x) : f (1 / 4) + f (3 / 4) = 1 := by sorry
Source
If , find .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3415 (f : ℝ → ℝ) (hf : ∀ x, f (f x) = 1 - x) : f (1 / 4) + f (3 / 4) = 1 := by sorry