lean_workbook_plus_34320

Proved

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

Find all continous function $f :R^{+} \longrightarrow R^{+}$ such that:\n\n $i) f(f(x)) =x$ \n\n $ii) f(x+1)=\dfrac{f(x)}{f(x)+1}$ $\forall x >0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34320 (f : ℝ → ℝ) (hf: Continuous f) (hf1: ∀ x>0, f (f x) = x) (hf2: ∀ x>0, f (x + 1) = f x / (f x + 1)) : ∀ x>0, f x = 1 / (x+1)   :=  by sorry

Source

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

View graph