An iterated recurrence fixes its input

Proved

WorkbookSource.problem_45573

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

We prove by induction that $f(x,n)=x$ . It is true for our base case $n=0$ . Now suppose it is true up to $n=m$ . Notice that

f(x,m+1)=f(f(x,m),m)=f(x,m)=x

so it is true for all natural $n$ .

Source: InternLM Lean-Workbook, record lean_workbook_45573 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_45573 (f : ℕ → ℕ → ℕ) (x : ℕ) (n : ℕ)
  (h₀ : ∀ x, f x 0 = x)
  (h₁ : ∀ x n, f x (n + 1) = f (f x n) n) :
  f x n = x  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_45573; Apache-2.0

View graph