lean_workbook_plus_68008

Proved

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

We got that $f(x+y)-x-y=f(x)-x$ and so $f(u)-u=f(v)-v$ whatever are $u\\ne v$ , still true when $u=v$ . And so $f(x)-x$ is constant. And so $f(x)=x+a$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68008 (f : ℝ → ℝ) (h : ∀ x y, (x + y) - f (x + y) = x - f x) : ∃ a, ∀ x, f x = x + a   :=  by sorry

Source

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

View graph