lean_workbook_plus_71508

Proved

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

$P(x,-2x)$ $\implies$ $f(x)f(-x)=1-xf(-x)+x$ \n $P(-x,2x)$ $\implies$ $f(x)f(-x)=1+xf(x)-x$ \nSubtracting, we get $f(-x)=2-f(x)$ $\forall x\ne 0$ , still true when $x=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71508  (x : ℝ)
  (f : ℝ → ℝ)
  (h₀ : x ≠ 0)
  (h₁ : 2 * f x * f (-x) = 2 - x * f (-x) + x)
  (h₂ : 2 * f x * f (-x) = 2 + x * f x - x) :
  f (-x) = 2 - f x   :=  by sorry

Source

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

View graph