Prove2Me

lean_workbook_plus_74641

Proved

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

Find all continuous function f;R→R f;R \to R such that f(αx+βy)=αf(x)+βf(y),∀x,y,∈R f( \alpha x+ \beta y) = \alpha f(x) + \beta f(y), \forall x,y, \in R given α+β=1 \alpha + \beta = 1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74641 (α β : ℝ) (h : α + β = 1) : ∃ f : ℝ → ℝ, Continuous f ∧ ∀ x y : ℝ, f (α * x + β * y) = α * f x + β * f y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph