lean_workbook_plus_66680

Proved

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

If $f(0) = 0$ , then $f(x)^3 = f(x)^2$ , so $f(x) = 0$ or $f(x) = 1$ for any $x$ . Also, the statement in the problem becomes $f(x)+f(y) = f(x+y)$ . Suppose $f(a) = 1$ for some $a$ , then $f(2a) = f(a) + f(a) = 1+1 = 2$ , contradiction. So $f(x) = 0$ for all $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66680  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = 0 ∨ ∀ x, f x = 1)
  (h₁ : ∀ x y, f (x + y) = f x + f y)
  (h₂ : f 0 = 0) :
  ∀ x, f x = 0   :=  by sorry

Source

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

View graph