lean_workbook_plus_72264

Proved

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

Assume that there are finitely many $n$ satisfying $f(n) = n$ . This implies that there exists some $N \in \mathbb{N}$ such that for all $n \geq N$ , $f(n) \neq n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72264 (f : ℕ → ℕ) (hf : Set.Finite {n | f n = n}) : ∃ N, ∀ n ≥ N, f n ≠ n   :=  by sorry

Source

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

View graph