lean_workbook_plus_82330

Proved

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

proofwiki

Find all functions $f:R\rightarrow R$ such that $f(x-f(y))=1-x-y$ , for all $x,y\in{\mathbb{R}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82330 (f : ℝ → ℝ): (∀ x y, f (x - f y) = 1 - x - y) ↔ ∀ x, f x = 1 / 2 - x   :=  by sorry

Source