lean_workbook_plus_3883

Proved

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

Find the number of functions $f: (1,2 \cdots n) \to (1,2,3,4,5)$ such that for any $k=1,2 \cdots n-1$ , we have $|f(k+1)-f(k)| \ge 3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3883 (n : ℕ) : ∃ F : ℕ → ℕ, ∀ k : ℕ, k ≤ n - 1 → F (k + 1) - F k ≥ 3   :=  by sorry

Source