lean_workbook_plus_10589

Proved

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

Find all continuous functions $f:[0;1]\to\mathbb{R}$ such that $f(x^2)+f(x)=x,\forall x\in [0;1]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10589 (f : ℝ → ℝ) (hf: ContinuousOn f (Set.Icc 0 1)) (hx: ∀ x ∈ (Set.Icc 0 1), f (x^2) + f x = x) : ∀ x ∈ (Set.Icc 0 1), f x = x - x^2   :=  by sorry

Source

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

View graph