lean_workbook_plus_81133

Proved

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

Let $f:\mathbb{R}\to\mathbb{R}$ be a function such that $f\left ( \frac{x+y}{3} \right )=\frac{f(x)+f(y)}{2}$ . Prove that the function $g:\mathbb{R}\to\mathbb{R}$ , $g(x)=f(x)-f(0)$ is additive.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81133 (f : ℝ → ℝ) (hf : ∀ x y, f ((x + y) / 3) = (f x + f y) / 2) :
    ∀ x y, f (x + y) - f 0 = f x - f 0 + (f y - f 0)   :=  by sorry

Source

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

View graph