lean_workbook_plus_49092
ProvedFind a continuous function such that for all and for all , the following functional equation holds: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49092 (A : Set ℝ) : ∃ f : ℝ → ℝ, Continuous f ∧ ∀ a ∈ A, ∀ b, f (a + b) + f (a - b) = 2 * f a := by sorry
Source