Dedekind real numbers
Content created by Egbert Rijke, Elif Uskuplu and Fredrik Bakke.
Created on 2023-04-08.
Last modified on 2023-04-28.
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 foundation.dependent-pair-types open import foundation.disjunction open import foundation.existential-quantification open import foundation.logical-equivalences open import foundation.negation open import foundation.propositions open import foundation.sets open import foundation.truncated-types open import foundation.universe-levels open import foundation-core.truncation-levels
Idea
A Dedekind cut consists a pair (L , U)
of subtypes of ℚ
, 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
is-dedekind-cut-Prop : {l : Level} → (ℚ → Prop l) → (ℚ → Prop l) → Prop l is-dedekind-cut-Prop L U = prod-Prop ( prod-Prop (exists-Prop ℚ L) (exists-Prop ℚ U)) ( prod-Prop ( prod-Prop ( Π-Prop ℚ ( λ q → iff-Prop ( L q) ( exists-Prop ℚ (λ r → prod-Prop (le-ℚ-Prop q r) (L r))))) ( Π-Prop ℚ ( λ r → iff-Prop ( U r) ( exists-Prop ℚ (λ q → prod-Prop (le-ℚ-Prop q r) (U q)))))) ( prod-Prop ( Π-Prop ℚ (λ q → neg-Prop (prod-Prop (L q) (U q)))) ( Π-Prop ℚ ( λ q → Π-Prop ℚ ( λ r → implication-Prop ( le-ℚ-Prop q r) ( disj-Prop (L q) (U r))))))) is-dedekind-cut : {l : Level} → (ℚ → Prop l) → (ℚ → Prop l) → UU l is-dedekind-cut L U = type-Prop (is-dedekind-cut-Prop L U)
The Dedekind real numbers
ℝ : (l : Level) → UU (lsuc l) ℝ l = Σ (ℚ → Prop l) (λ L → Σ (ℚ → Prop l) (is-dedekind-cut L))
ℝ is 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) pr1 (ℝ-Set l) = ℝ l pr2 (ℝ-Set l) = is-set-ℝ l
Recent changes
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-04-26. Elif Uskuplu and Egbert Rijke. Countability results (#569).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).