lean_workbook_plus_2728
Proved, which indeed fits
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2728 : ∃ f : ℝ → ℝ, ∀ x, f x = -1 := by sorry
Source
, which indeed fits
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2728 : ∃ f : ℝ → ℝ, ∀ x, f x = -1 := by sorry