lean_workbook_plus_24120

Proved

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

$\therefore f(y) = \alpha +y, \forall y \in \mathbb{R}$ >> which is clearly a solution where $\alpha \in \mathbb{R}$ is any constant.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24120 (f : ℝ → ℝ) (hf: f = fun (y:ℝ) ↦ y + f 0) : ∃ (α : ℝ), ∀ (y : ℝ), f y = α + y   :=  by sorry

Source