lean_workbook_plus_78160

Proved

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

$P\left( {x, - x} \right) \Rightarrow f\left( 0 \right) + 2f\left( {2x} \right) = 3f\left( x \right) + x\,\,\,\,\,\,(2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78160 (x : ℝ) (f : ℝ → ℝ) (h₁ : ∀ x, f (-x) = f x) (h₂ : ∀ x, f (2 * x) = 3 * f x + x) : f 0 + 2 * f (2 * x) = 3 * f x + x   :=  by sorry

Source

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

View graph