lean_workbook_plus_29720

Proved

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

So $f(x+c)=ax+b$ $\forall x>0$ and so $f(x)=ax+d$ $\forall x>c$ (where $d=b-ac$ )

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29720 (f : ℝ → ℝ) (a b c : ℝ) (hf: ∀ x > 0, f (x + c) = a * x + b) : ∃ d, ∀ x > c, f x = a * x + d   :=  by sorry

Source