lean_workbook_plus_38133

Proved

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

Find all functions $f(x)$ from the set $S = \{ 1, 2, 3, 4, 5 \}$ to itself such that $f(f(x)) = x$ for all $x \in S$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38133 (S : Finset ℕ) (hS : S = {1, 2, 3, 4, 5}) : ∃ f : ℕ → ℕ, ∀ x ∈ S, f (f x) = x   :=  by sorry

Source