lean_workbook_plus_2151

Proved

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

Prove that $f(x) = \frac{1}{cx + 1}$ for all $x > 0$ where $c \geq 0$ is a constant is a solution to the functional equation $f(x)f(yf(x)) = f(x + y)$ for all $x, y > 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2151 (c : ℝ) (hc : 0 ≤ c) (f : ℝ → ℝ) (hf: ∀ x, f x = 1 / (c * x + 1)) : ∀ x y, (x > 0 ∧ y > 0) → f x * f (y * f x) = f (x + y)   :=  by sorry

Source

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

View graph