lean_workbook_plus_25579

Proved

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

Find all continuous functions $f:\left(0,\infty\right)\rightarrow\mathbb{R}$ having the property that : \n\n $f\left(x\right)+pf\left(px\right)=1,p>1,fixed$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25579 (p : ℝ) (hp : p > 1) (hf: ∀ x : ℝ, 0 < x → ∃ y : ℝ, y + p * y = 1) : ∃ f : ℝ → ℝ, Continuous f ∧ ∀ x : ℝ, 0 < x → f x + p * f (p * x) = 1   :=  by sorry

Source

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

View graph