lean_workbook_plus_3284
ProvedAnd so which indeed is a solution, whatever is
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3284 (f : ℝ → ℝ) (c : ℝ) (h : ∀ x, f x = c) : ∀ x, f x = c := by sorry
Source
And so which indeed is a solution, whatever is
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3284 (f : ℝ → ℝ) (c : ℝ) (h : ∀ x, f x = c) : ∀ x, f x = c := by sorry