lean_workbook_plus_3343

Proved

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

f(1)=2 $P(x,1)\implies f(x+1)+f(x)=1,\quad\forall x\in\mathbb{R}\implies f(x+2)=f(x),\quad\forall x\in\mathbb{R}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3343 (f : ℝ → ℝ) (hf1 : f 1 = 2) (hf2 : ∀ x, f (x + 1) + f x = 1) : ∀ x, f (x + 2) = f x   :=  by sorry

Source