lean_workbook_plus_55943
ProvedS2:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55943 : ∃ f : ℝ → ℝ, f 0 = 1 ∧ ∀ x > 0, f x = 0 := by sorry
Source
S2:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_55943 : ∃ f : ℝ → ℝ, f 0 = 1 ∧ ∀ x > 0, f x = 0 := by sorry