by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let be a,b∈R and let be f:R→R such that a⋅f(x)+b⋅f(1−x)=x(1),(∀)x∈R .\n\ni)Show that f(x)+f(1−x)=a+b1,(∀)x∈R,a=−b ;\n\nii)If a=b , prove that (∄)f satisfying (1) ;\n\nii)If a=b , find f .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60103 (a b : ℝ) (f : ℝ → ℝ) (h₁ : a ≠ -b) (h₂ : ∀ x, a * f x + b * f (1 - x) = x) : ∀ x, f x + f (1 - x) = 1 / (a + b) := by sorry