lean_workbook_plus_65340

Proved

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

The function $f$ satisfies, for all $x$ , the equation $f(x) + (1-x) f(-x) = x^{2}$ . Show that $f(-x) + (1+ x)f(x) = x^{2}$ .Hence find $f(x)$ in terms of $x$ . You should verify that your function satisfies the original equation.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65340 (f : ℝ → ℝ) (hf: ∀ x, f x + (1 - x) * f (-x) = x^2) : ∀ x, f (-x) + (1 + x) * f x = x^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph