lean_workbook_plus_58081

Proved

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

Find continuous $f:\mathbb{R}\longrightarrow\mathbb{R},$ with $\forall x,y,z, \; f(\frac {x+2y}3)+f(\frac {y+2z}3)+f(\frac {z+2x}3)=f(x)+f(y)+ f(z)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58081 : ∃ f : ℝ → ℝ, Continuous f ∧ ∀ x y z : ℝ, f ((x + 2 * y) / 3) + f ((y + 2 * z) / 3) + f ((z + 2 * x) / 3) = f x + f y + f z   :=  by sorry

Source

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

View graph