Two functional relations force the zero function

Proved

WorkbookSource.problem_6261

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

$P(x,-1)\implies f(x-1)=f(-x).P(x-1,1)\implies f(x)=3f(x-1)$ . Substituting $f(x-1)$ from first into the second yields

f(x)=3f(-x).

Let $x=x$ and $x=-x$ into the past function to get $f(x)=3f(-x)$ and $f(-x)=3f(x).$ Substituting the $f(-x)$ from the second into the first yields $f(x)=3f(-x)=3(3f(x))=9f(x)\implies \boxed{f(x)=0}.$ We can easily check that this function works.

Source: InternLM Lean-Workbook, record lean_workbook_6261 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_6261  (f : ℝ → ℝ)
  (h₀ : ∀ x, f (x - 1) = f (-x))
  (h₁ : ∀ x, f x = 3 * f (x - 1)) :
  f = λ _ => 0  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_6261; Apache-2.0

View graph