Prove2Me

lean_workbook_plus_10787

Proved

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

Given the system of equations: \n{g(x)=h(x)+k(x) g(−x)=h(x)−k(x) \begin{cases}g(x)=h(x)+k(x) \\\ g(-x)=h(x)-k(x) \end{cases} \nShow that h(x)=g(x)+g(−x)2 h(x)=\frac{g(x)+g(-x)}{2} and k(x)=g(x)−g(−x)2 k(x)=\frac{g(x)-g(-x)}{2} satisfy the conditions and prove their uniqueness.

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

View graph