lean_workbook_plus_74287
DisprovedUsing the Dedekind Cut definition, prove the existence and uniqueness of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74287 : ∃! x : ℝ, x ^ 2 = 2 := by sorry
Source
Using the Dedekind Cut definition, prove the existence and uniqueness of .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_74287 : ∃! x : ℝ, x ^ 2 = 2 := by sorry