Dedekinds_Theorem
Provedanalysisdedekind-cutproofwikireal-numbers
Let be a Dedekind cut of the set of real numbers . Then there exists a unique real number which is a producer of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Dedekinds_Theorem (L R : Set ℝ) (hL : L.Nonempty) (hR : R.Nonempty) (hpart : L ∪ R = Set.univ) (hdisj : Disjoint L R) (hord : ∀ l ∈ L, ∀ r ∈ R, l < r) : ∃! x : ℝ, ∀ l ∈ L, ∀ r ∈ R, l ≤ x ∧ x ≤ r := by sorry
Source