lean_workbook_plus_60842

Proved

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

Then $f(x)=1-f(0)-x$ , and $f(0)=1-f(0)$ hence $f(0)=1/2$ . and $f(x)=\frac 12-x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60842 (f : ℝ → ℝ) (hf: f = fun (x:ℝ) => 1 - f 0 - x) : f 0 = 1 / 2 ∧ f = fun (x:ℝ) => 1 / 2 - x   :=  by sorry

Source