lean_workbook_plus_70548

Proved

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

$f(2n)=a-2n$ and $f(2n+1)=b-(2n+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70548 (a b : ℤ) (f : ℤ → ℤ) (h₁ : ∀ n : ℕ, f (2 * n) = a - 2 * n) (h₂ : ∀ n : ℕ, f (2 * n + 1) = b - (2 * n + 1)) : ∃ a b : ℤ, ∀ n : ℕ, f n = if n % 2 = 0 then a - n else b - n   :=  by sorry

Source

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

View graph