lean_workbook_plus_9493

Proved

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

From $f(x-f(2x))+x=0$ and $f(2x)=f(x)+x$ we obtain $f(-f(x))=-x$ for all $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9493 (f : ℝ → ℝ): (∀ x, f (2 * x) = f x + x) ∧ (∀ x, f (x - f (2 * x)) + x = 0) → ∀ x, f (-f x) = -x   :=  by sorry

Source