lean_workbook_plus_52051

Proved

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

Prove that any function $g$ can be written in the form $g=h+k$ where $h$ is an even function and $k$ is an odd function.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52051 (g : ℝ → ℝ) : ∃ h k : ℝ → ℝ, Even h ∧ Odd k ∧ g = h + k   :=  by sorry

Source