lean_workbook_plus_1042
DisprovedProve that there is no function satisfying
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1042 : ¬∃ f : ℕ → ℕ, ∀ n, f (f n) = f (n + 1) - f n := by sorry
Source
Prove that there is no function satisfying
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1042 : ¬∃ f : ℕ → ℕ, ∀ n, f (f n) = f (n + 1) - f n := by sorry