lean_workbook_plus_22141

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $f(x)$ is a function, $f(x) + f(1-x) = 11$ and $f(1+x) = 3 + f(x)$ , find $f(x) + f(-x)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22141 (f : ℝ → ℝ) (hf : ∀ x, f x + f (1 - x) = 11) (hf' : ∀ x, f (1 + x) = 3 + f x) : ∀ x, f x + f (-x) = 8   :=  by sorry

Source