Dedekind real numbers
Content created by Fredrik Bakke, Egbert Rijke, malarbol, Elif Uskuplu and Vojtěch Štěpančík.
Created on 2023-04-08.
Last modified on 2024-04-11.
module real-numbers.dedekind-real-numbers where
Imports
open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.complements-subtypes open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.embeddings open import foundation.empty-types open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.universal-quantification open import foundation.universe-levels open import foundation-core.truncation-levels
Idea
A
Dedekind cut¶
consists of a pair (L , U)
of
subtypes of
the rational numbers ℚ
,
satisfying the following four conditions
- Inhabitedness. Both
L
andU
are inhabited subtypes ofℚ
. - Roundedness. A rational number
q
is inL
if and only if there existsq < r
such thatr ∈ L
, and a rational numberr
is inU
if and only if there existsq < r
such thatq ∈ U
. - Disjointness.
L
andU
are disjoint subsets ofℚ
. - Locatedness. If
q < r
thenq ∈ L
orr ∈ U
.
The type of Dedekind real numbers¶ is the type of all
Dedekind cuts. The Dedekind real numbers will be taken as the standard
definition of the real numbers in the agda-unimath
library.
Definition
Dedekind cuts
module _ {l1 l2 : Level} (L : subtype l1 ℚ) (U : subtype l2 ℚ) where is-dedekind-cut-Prop : Prop (l1 ⊔ l2) is-dedekind-cut-Prop = conjunction-Prop ( (∃ ℚ L) ∧ (∃ ℚ U)) ( conjunction-Prop ( conjunction-Prop ( ∀' ℚ ( λ q → L q ⇔ ∃ ℚ (λ r → le-ℚ-Prop q r ∧ L r))) ( ∀' ℚ ( λ r → U r ⇔ ∃ ℚ (λ q → le-ℚ-Prop q r ∧ U q)))) ( conjunction-Prop ( ∀' ℚ (λ q → ¬' (L q ∧ U q))) ( ∀' ℚ (λ q → ∀' ℚ (λ r → le-ℚ-Prop q r ⇒ (L q ∨ U r)))))) is-dedekind-cut : UU (l1 ⊔ l2) is-dedekind-cut = type-Prop is-dedekind-cut-Prop is-prop-is-dedekind-cut : is-prop is-dedekind-cut is-prop-is-dedekind-cut = is-prop-type-Prop is-dedekind-cut-Prop
The Dedekind real numbers
ℝ : (l : Level) → UU (lsuc l) ℝ l = Σ (subtype l ℚ) (λ L → Σ (subtype l ℚ) (is-dedekind-cut L)) real-dedekind-cut : {l : Level} (L U : subtype l ℚ) → is-dedekind-cut L U → ℝ l real-dedekind-cut L U H = L , U , H module _ {l : Level} (x : ℝ l) where lower-cut-ℝ : subtype l ℚ lower-cut-ℝ = pr1 x upper-cut-ℝ : subtype l ℚ upper-cut-ℝ = pr1 (pr2 x) is-in-lower-cut-ℝ : ℚ → UU l is-in-lower-cut-ℝ = is-in-subtype lower-cut-ℝ is-in-upper-cut-ℝ : ℚ → UU l is-in-upper-cut-ℝ = is-in-subtype upper-cut-ℝ is-dedekind-cut-cut-ℝ : is-dedekind-cut lower-cut-ℝ upper-cut-ℝ is-dedekind-cut-cut-ℝ = pr2 (pr2 x) is-inhabited-lower-cut-ℝ : exists ℚ lower-cut-ℝ is-inhabited-lower-cut-ℝ = pr1 (pr1 is-dedekind-cut-cut-ℝ) is-inhabited-upper-cut-ℝ : exists ℚ upper-cut-ℝ is-inhabited-upper-cut-ℝ = pr2 (pr1 is-dedekind-cut-cut-ℝ) is-rounded-lower-cut-ℝ : (q : ℚ) → is-in-lower-cut-ℝ q ↔ exists ℚ (λ r → (le-ℚ-Prop q r) ∧ (lower-cut-ℝ r)) is-rounded-lower-cut-ℝ = pr1 (pr1 (pr2 is-dedekind-cut-cut-ℝ)) is-rounded-upper-cut-ℝ : (r : ℚ) → is-in-upper-cut-ℝ r ↔ exists ℚ (λ q → (le-ℚ-Prop q r) ∧ (upper-cut-ℝ q)) is-rounded-upper-cut-ℝ = pr2 (pr1 (pr2 is-dedekind-cut-cut-ℝ)) is-disjoint-cut-ℝ : (q : ℚ) → ¬ (is-in-lower-cut-ℝ q × is-in-upper-cut-ℝ q) is-disjoint-cut-ℝ = pr1 (pr2 (pr2 is-dedekind-cut-cut-ℝ)) is-located-lower-upper-cut-ℝ : (q r : ℚ) → le-ℚ q r → type-disjunction-Prop (lower-cut-ℝ q) (upper-cut-ℝ r) is-located-lower-upper-cut-ℝ = pr2 (pr2 (pr2 is-dedekind-cut-cut-ℝ)) cut-ℝ : subtype l ℚ cut-ℝ q = coproduct-Prop ( lower-cut-ℝ q) ( upper-cut-ℝ q) ( ev-pair ( is-disjoint-cut-ℝ q)) is-in-cut-ℝ : ℚ → UU l is-in-cut-ℝ = is-in-subtype cut-ℝ
Properties
The Dedekind real numbers form a set
abstract is-set-ℝ : (l : Level) → is-set (ℝ l) is-set-ℝ l = is-set-Σ ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋)) ( λ x → is-set-Σ ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋)) ( λ y → ( is-set-is-prop ( is-prop-type-Prop ( is-dedekind-cut-Prop x y))))) ℝ-Set : (l : Level) → Set (lsuc l) ℝ-Set l = ℝ l , is-set-ℝ l
Properties of lower/upper Dedekind cuts
Lower and upper Dedekind cuts are closed under the standard ordering on the rationals
module _ {l : Level} (x : ℝ l) (p q : ℚ) where le-lower-cut-ℝ : le-ℚ p q → is-in-lower-cut-ℝ x q → is-in-lower-cut-ℝ x p le-lower-cut-ℝ H H' = ind-trunc-Prop ( λ s → lower-cut-ℝ x p) ( rec-coproduct ( id) ( λ I → ex-falso (is-disjoint-cut-ℝ x q (H' , I)))) ( is-located-lower-upper-cut-ℝ x p q H) leq-lower-cut-ℝ : leq-ℚ p q → is-in-lower-cut-ℝ x q → is-in-lower-cut-ℝ x p leq-lower-cut-ℝ H H' = rec-coproduct ( λ s → le-lower-cut-ℝ s H') ( λ I → tr ( is-in-lower-cut-ℝ x) ( antisymmetric-leq-ℚ q p I H) ( H')) ( decide-le-leq-ℚ p q) le-upper-cut-ℝ : le-ℚ p q → is-in-upper-cut-ℝ x p → is-in-upper-cut-ℝ x q le-upper-cut-ℝ H H' = ind-trunc-Prop ( λ s → upper-cut-ℝ x q) ( rec-coproduct ( λ I → ex-falso (is-disjoint-cut-ℝ x p ( I , H'))) ( id)) ( is-located-lower-upper-cut-ℝ x p q H) leq-upper-cut-ℝ : leq-ℚ p q → is-in-upper-cut-ℝ x p → is-in-upper-cut-ℝ x q leq-upper-cut-ℝ H H' = rec-coproduct ( λ s → le-upper-cut-ℝ s H') ( λ I → tr ( is-in-upper-cut-ℝ x) ( antisymmetric-leq-ℚ p q H I) ( H')) ( decide-le-leq-ℚ p q)
Elements of the lower cut are lower bounds of the upper cut
module _ {l : Level} (x : ℝ l) (p q : ℚ) where le-lower-upper-cut-ℝ : is-in-lower-cut-ℝ x p → is-in-upper-cut-ℝ x q → le-ℚ p q le-lower-upper-cut-ℝ H H' = rec-coproduct ( id) ( λ I → ex-falso ( is-disjoint-cut-ℝ x p ( H , leq-upper-cut-ℝ x q p I H'))) ( decide-le-leq-ℚ p q)
Characterisation of each cut by the other
The lower cut is the subtype of rationals bounded above by some element of the complement of the upper cut
module _ {l : Level} (x : ℝ l) where is-lower-complement-upper-cut-ℝ-Prop : (p q : ℚ) → Prop l is-lower-complement-upper-cut-ℝ-Prop p q = ( le-ℚ-Prop p q) ∧ (¬' (upper-cut-ℝ x q)) lower-complement-upper-cut-ℝ : subtype l ℚ lower-complement-upper-cut-ℝ p = ∃ ℚ (is-lower-complement-upper-cut-ℝ-Prop p)
module _ {l : Level} (x : ℝ l) where subset-lower-cut-lower-complement-upper-cut-ℝ : lower-complement-upper-cut-ℝ x ⊆ lower-cut-ℝ x subset-lower-cut-lower-complement-upper-cut-ℝ p = elim-exists ( lower-cut-ℝ x p) ( λ q I → map-right-unit-law-disjunction-is-empty-Prop ( lower-cut-ℝ x p) ( upper-cut-ℝ x q) ( pr2 I) ( is-located-lower-upper-cut-ℝ x p q ( pr1 I))) subset-lower-complement-upper-cut-lower-cut-ℝ : lower-cut-ℝ x ⊆ lower-complement-upper-cut-ℝ x subset-lower-complement-upper-cut-lower-cut-ℝ p H = elim-exists ( lower-complement-upper-cut-ℝ x p) ( λ q I → intro-exists ( q) ( map-product ( id) ( λ L U → is-disjoint-cut-ℝ x q (L , U)) ( I))) ( pr1 (is-rounded-lower-cut-ℝ x p) H) eq-lower-cut-lower-complement-upper-cut-ℝ : lower-complement-upper-cut-ℝ x = lower-cut-ℝ x eq-lower-cut-lower-complement-upper-cut-ℝ = antisymmetric-leq-subtype ( lower-complement-upper-cut-ℝ x) ( lower-cut-ℝ x) ( subset-lower-cut-lower-complement-upper-cut-ℝ) ( subset-lower-complement-upper-cut-lower-cut-ℝ)
The upper cut is the subtype of rationals bounded below by some element of the complement of the lower cut
module _ {l : Level} (x : ℝ l) where is-upper-complement-lower-cut-ℝ-Prop : (q p : ℚ) → Prop l is-upper-complement-lower-cut-ℝ-Prop q p = (le-ℚ-Prop p q) ∧ (¬' (lower-cut-ℝ x p)) upper-complement-lower-cut-ℝ : subtype l ℚ upper-complement-lower-cut-ℝ q = ∃ ℚ (is-upper-complement-lower-cut-ℝ-Prop q)
module _ {l : Level} (x : ℝ l) where subset-upper-cut-upper-complement-lower-cut-ℝ : upper-complement-lower-cut-ℝ x ⊆ upper-cut-ℝ x subset-upper-cut-upper-complement-lower-cut-ℝ q = elim-exists ( upper-cut-ℝ x q) ( λ p I → map-left-unit-law-disjunction-is-empty-Prop ( lower-cut-ℝ x p) ( upper-cut-ℝ x q) ( pr2 I) ( is-located-lower-upper-cut-ℝ x p q ( pr1 I))) subset-upper-complement-lower-cut-upper-cut-ℝ : upper-cut-ℝ x ⊆ upper-complement-lower-cut-ℝ x subset-upper-complement-lower-cut-upper-cut-ℝ q H = elim-exists ( upper-complement-lower-cut-ℝ x q) ( λ p I → intro-exists ( p) ( map-product ( id) ( λ U L → is-disjoint-cut-ℝ x p (L , U)) ( I))) ( pr1 (is-rounded-upper-cut-ℝ x q) H) eq-upper-cut-upper-complement-lower-cut-ℝ : upper-complement-lower-cut-ℝ x = upper-cut-ℝ x eq-upper-cut-upper-complement-lower-cut-ℝ = antisymmetric-leq-subtype ( upper-complement-lower-cut-ℝ x) ( upper-cut-ℝ x) ( subset-upper-cut-upper-complement-lower-cut-ℝ) ( subset-upper-complement-lower-cut-upper-cut-ℝ)
The lower/upper cut of a real determines the other
module _ {l : Level} (x y : ℝ l) where subset-lower-cut-upper-cut-ℝ : upper-cut-ℝ y ⊆ upper-cut-ℝ x → lower-cut-ℝ x ⊆ lower-cut-ℝ y subset-lower-cut-upper-cut-ℝ H = binary-tr ( _⊆_) ( eq-lower-cut-lower-complement-upper-cut-ℝ x) ( eq-lower-cut-lower-complement-upper-cut-ℝ y) ( λ p → elim-exists ( lower-complement-upper-cut-ℝ y p) ( λ q → intro-exists q ∘ tot (λ _ K → K ∘ H q))) subset-upper-cut-lower-cut-ℝ : lower-cut-ℝ x ⊆ lower-cut-ℝ y → upper-cut-ℝ y ⊆ upper-cut-ℝ x subset-upper-cut-lower-cut-ℝ H = binary-tr ( _⊆_) ( eq-upper-cut-upper-complement-lower-cut-ℝ y) ( eq-upper-cut-upper-complement-lower-cut-ℝ x) ( λ q → elim-exists ( upper-complement-lower-cut-ℝ x q) ( λ p → intro-exists p ∘ tot (λ _ K → K ∘ H p))) module _ {l : Level} (x y : ℝ l) where eq-lower-cut-eq-upper-cut-ℝ : upper-cut-ℝ x = upper-cut-ℝ y → lower-cut-ℝ x = lower-cut-ℝ y eq-lower-cut-eq-upper-cut-ℝ H = antisymmetric-leq-subtype ( lower-cut-ℝ x) ( lower-cut-ℝ y) ( subset-lower-cut-upper-cut-ℝ x y ( pr2 ∘ has-same-elements-eq-subtype ( upper-cut-ℝ x) ( upper-cut-ℝ y) ( H))) ( subset-lower-cut-upper-cut-ℝ y x ( pr1 ∘ has-same-elements-eq-subtype ( upper-cut-ℝ x) ( upper-cut-ℝ y) ( H))) eq-upper-cut-eq-lower-cut-ℝ : lower-cut-ℝ x = lower-cut-ℝ y → upper-cut-ℝ x = upper-cut-ℝ y eq-upper-cut-eq-lower-cut-ℝ H = antisymmetric-leq-subtype ( upper-cut-ℝ x) ( upper-cut-ℝ y) ( subset-upper-cut-lower-cut-ℝ y x ( pr2 ∘ has-same-elements-eq-subtype ( lower-cut-ℝ x) ( lower-cut-ℝ y) ( H))) ( subset-upper-cut-lower-cut-ℝ x y ( pr1 ∘ has-same-elements-eq-subtype ( lower-cut-ℝ x) ( lower-cut-ℝ y) ( H)))
The map from a real number to its lower cut is an embedding
module _ {l : Level} (L : subtype l ℚ) where has-upper-cut-Prop : Prop (lsuc l) has-upper-cut-Prop = pair ( Σ (subtype l ℚ) (is-dedekind-cut L)) ( is-prop-all-elements-equal ( λ U U' → eq-type-subtype ( is-dedekind-cut-Prop L) ( eq-upper-cut-eq-lower-cut-ℝ ( pair L U) ( pair L U') ( refl)))) is-emb-lower-cut : {l : Level} → is-emb (lower-cut-ℝ {l}) is-emb-lower-cut = is-emb-inclusion-subtype has-upper-cut-Prop
Two real numbers with the same lower/upper cut are equal
module _ {l : Level} (x y : ℝ l) where eq-eq-lower-cut-ℝ : lower-cut-ℝ x = lower-cut-ℝ y → x = y eq-eq-lower-cut-ℝ = eq-type-subtype has-upper-cut-Prop eq-eq-upper-cut-ℝ : upper-cut-ℝ x = upper-cut-ℝ y → x = y eq-eq-upper-cut-ℝ = eq-eq-lower-cut-ℝ ∘ (eq-lower-cut-eq-upper-cut-ℝ x y)
References
This page follows parts of Section 11.2 in [UF13].
- [UF13]
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.
External links
- Dedekind cut at Mathswitch
- DedekindReals.Type at TypeTopology
- Dedekind cut at Lab
- Dedekind cut at Wikipedia
- Construction of the real numbers by Dedekind cuts at Wikipedia
- Dedekind cut at Britannica
Recent changes
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2024-03-28. malarbol and Fredrik Bakke. Refactoring positive integers (#1059).
- 2024-03-23. Vojtěch Štěpančík. Enhancements for the Concepts macro (#1093).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2024-02-27. malarbol. Rational real numbers (#1034).