lean_workbook_plus_14086
DisprovedShow that there does not exist a non constant continuous such that with .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14086 : ¬∃ f : ℝ × ℝ → ℝ, (∀ x : ℝ × ℝ, x.fst ^ 2 + x.snd ^ 2 < 1 → f x = 5) ∧ ¬∀ x y : ℝ × ℝ, f x = f y := by sorry
Source