Lower Dedekind real numbers

Content created by Louis Wasserman.

Created on 2025-02-16.
Last modified on 2025-02-16.

module real-numbers.lower-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.conjunction
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.powersets
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.truncation-levels
open import foundation.universal-quantification
open import foundation.universe-levels

Idea

A subtype L of the rational numbers is a lower Dedekind cut if it satisfies the following two conditions:

  1. Inhabitedness. L is inhabited.
  2. Lower roundedness. A rational number q is in L if and only if there exists q < r such that r ∈ L.

The lower Dedekind real numbers is the type of all lower Dedekind cuts.

Definition

Lower Dedekind cuts

module _
  {l : Level}
  (L : subtype l ℚ)
  where

  is-lower-dedekind-cut-Prop : Prop l
  is-lower-dedekind-cut-Prop =
    (∃ ℚ L) ∧
    (∀' ℚ (λ q → L q ⇔ (∃ ℚ (λ r → le-ℚ-Prop q r ∧ L r))))

  is-lower-dedekind-cut : UU l
  is-lower-dedekind-cut = type-Prop is-lower-dedekind-cut-Prop

The lower Dedekind real numbers

lower-ℝ : (l : Level) → UU (lsuc l)
lower-ℝ l = Σ (subtype l ℚ) is-lower-dedekind-cut

module _
  {l : Level}
  (x : lower-ℝ l)
  where

  cut-lower-ℝ : subtype l ℚ
  cut-lower-ℝ = pr1 x

  is-in-cut-lower-ℝ : ℚ → UU l
  is-in-cut-lower-ℝ = is-in-subtype cut-lower-ℝ

  is-lower-dedekind-cut-lower-ℝ : is-lower-dedekind-cut cut-lower-ℝ
  is-lower-dedekind-cut-lower-ℝ = pr2 x

  is-inhabited-cut-lower-ℝ : exists ℚ cut-lower-ℝ
  is-inhabited-cut-lower-ℝ = pr1 (pr2 x)

  is-rounded-cut-lower-ℝ :
    (q : ℚ) →
    is-in-cut-lower-ℝ q ↔ exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-lower-ℝ r)
  is-rounded-cut-lower-ℝ = pr2 (pr2 x)

Properties

The lower Dedekind reals form a set

abstract
  is-set-lower-ℝ : (l : Level) → is-set (lower-ℝ l)
  is-set-lower-ℝ l =
    is-set-Σ
      ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋))
      ( λ q → is-set-is-prop (is-prop-type-Prop (is-lower-dedekind-cut-Prop q)))

Lower Dedekind cuts are closed under strict inequality on the rationals

module _
  {l : Level} (x : lower-ℝ l) (p q : ℚ)
  where

  is-in-cut-le-ℚ-lower-ℝ :
    le-ℚ p q → is-in-cut-lower-ℝ x q → is-in-cut-lower-ℝ x p
  is-in-cut-le-ℚ-lower-ℝ p<q q<x =
    backward-implication
      ( is-rounded-cut-lower-ℝ x p)
      ( intro-exists q (p<q , q<x))

Lower Dedekind cuts are closed under inequality on the rationals

module _
  {l : Level} (x : lower-ℝ l) (p q : ℚ)
  where

  is-in-cut-leq-ℚ-lower-ℝ :
    leq-ℚ p q → is-in-cut-lower-ℝ x q → is-in-cut-lower-ℝ x p
  is-in-cut-leq-ℚ-lower-ℝ p≤q q<x with decide-le-leq-ℚ p q
  ... | inl p<q = is-in-cut-le-ℚ-lower-ℝ x p q p<q q<x
  ... | inr q≤p = tr (is-in-cut-lower-ℝ x) (antisymmetric-leq-ℚ q p q≤p p≤q) q<x

Two lower real numbers with the same cut are equal

module _
  {l : Level} (x y : lower-ℝ l)
  where

  eq-eq-cut-lower-ℝ : cut-lower-ℝ x ＝ cut-lower-ℝ y → x ＝ y
  eq-eq-cut-lower-ℝ = eq-type-subtype is-lower-dedekind-cut-Prop

  eq-sim-cut-lower-ℝ : sim-subtype (cut-lower-ℝ x) (cut-lower-ℝ y) → x ＝ y
  eq-sim-cut-lower-ℝ =
    eq-eq-cut-lower-ℝ ∘
    antisymmetric-sim-subtype (cut-lower-ℝ x) (cut-lower-ℝ y)

See also

References

This page follows the terminology used in the exercises of Section 11 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.

Recent changes