Prove2Me

lean_workbook_plus_12058

Proved

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

Given any function ff , the unique decomposition into even and odd parts is f(x)=(12f(x)+12f(−x))+(12f(x)−12f(−x))f(x)=\left(\frac12f(x)+\frac12f(-x)\right)+\left(\frac12f(x)-\frac12f(-x)\right)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12058 (f : ℝ → ℝ) : ∀ x, f x = (f x + f (-x)) / 2 + (f x - f (-x)) / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph