Closed intervals in the real numbers

Content created by Louis Wasserman.

Created on 2025-10-15.
Last modified on 2025-10-15.

module real-numbers.closed-intervals-real-numbers where
Imports 
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.additive-group-of-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.positive-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-positive-rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import metric-spaces.closed-subsets-metric-spaces
open import metric-spaces.complete-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces

open import order-theory.closed-intervals-large-posets

open import real-numbers.cauchy-completeness-dedekind-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.metric-space-of-real-numbers
open import real-numbers.rational-real-numbers

Idea

A closed interval in the real numbers is a closed interval in the large poset of the real numbers.

Definition

closed-interval-ℝ : (l : Level) → UU (lsuc l)
closed-interval-ℝ l = closed-interval-Large-Poset ℝ-Large-Poset l l

is-in-closed-interval-prop-ℝ :
  {l1 l2 : Level} → closed-interval-ℝ l1 → ℝ l2 → Prop (l1 ⊔ l2)
is-in-closed-interval-prop-ℝ =
  is-in-closed-interval-prop-Large-Poset ℝ-Large-Poset

is-in-closed-interval-ℝ :
  {l1 l2 : Level} → closed-interval-ℝ l1 → ℝ l2 → UU (l1 ⊔ l2)
is-in-closed-interval-ℝ =
  is-in-closed-interval-Large-Poset ℝ-Large-Poset

subtype-closed-interval-ℝ :
  {l1 : Level} (l : Level) → closed-interval-ℝ l1 → subtype (l1 ⊔ l) (ℝ l)
subtype-closed-interval-ℝ = subtype-closed-interval-Large-Poset ℝ-Large-Poset

lower-bound-closed-interval-ℝ : {l : Level} → closed-interval-ℝ l → ℝ l
lower-bound-closed-interval-ℝ =
  lower-bound-closed-interval-Large-Poset ℝ-Large-Poset

upper-bound-closed-interval-ℝ : {l : Level} → closed-interval-ℝ l → ℝ l
upper-bound-closed-interval-ℝ =
  upper-bound-closed-interval-Large-Poset ℝ-Large-Poset

Properties

The unit interval on the real numbers

unit-closed-interval-ℝ : closed-interval-ℝ lzero
unit-closed-interval-ℝ =
  ((zero-ℝ , one-ℝ) , preserves-leq-real-ℚ zero-ℚ one-ℚ leq-zero-one-ℚ)

Closed intervals in the real numbers are closed in the metric space of real numbers

opaque
  unfolding leq-ℝ neighborhood-ℝ

  is-closed-subset-closed-interval-ℝ :
    {l1 l2 : Level} → ([a,b] : closed-interval-ℝ l1) →
    is-closed-subset-Metric-Space
      ( metric-space-ℝ l2)
      ( subtype-closed-interval-ℝ l2 [a,b])
  is-closed-subset-closed-interval-ℝ ((a , b) , a≤b) x H =
    ( ( λ q q<a →
        let open do-syntax-trunc-Prop (lower-cut-ℝ x q)
        in do
          (r , q<r , r<a) ← forward-implication (is-rounded-lower-cut-ℝ a q) q<a
          let ε⁺@(ε , _) = positive-diff-le-ℚ q r q<r
          (y , Nεxy , a≤y , _) ← H ε⁺
          pr1 Nεxy
            ( q)
            ( a≤y
              ( q +ℚ ε)
              ( inv-tr
                ( is-in-lower-cut-ℝ a)
                ( is-identity-right-conjugation-add-ℚ q r)
                ( r<a)))) ,
      ( λ q q<x →
        let open do-syntax-trunc-Prop (lower-cut-ℝ b q)
        in do
          (r , q<r , r<x) ← forward-implication (is-rounded-lower-cut-ℝ x q) q<x
          let ε⁺@(ε , _) = positive-diff-le-ℚ q r q<r
          (y , Nεxy , _ , y≤b) ← H ε⁺
          y≤b
            ( q)
            ( pr2 Nεxy
              ( q)
              ( inv-tr
                ( is-in-lower-cut-ℝ x)
                ( is-identity-right-conjugation-add-ℚ q r)
                ( r<x)))))

The metric space associated with a closed interval in ℝ

closed-subset-closed-interval-ℝ :
  {l1 : Level} (l : Level) → closed-interval-ℝ l1 →
  closed-subset-Metric-Space (l1 ⊔ l) (metric-space-ℝ l)
closed-subset-closed-interval-ℝ l [a,b] =
  ( subtype-closed-interval-ℝ l [a,b] ,
    is-closed-subset-closed-interval-ℝ [a,b])

metric-space-closed-interval-ℝ :
  {l1 : Level} (l : Level) → closed-interval-ℝ l1 →
  Metric-Space (l1 ⊔ lsuc l) l
metric-space-closed-interval-ℝ l [a,b] =
  subspace-closed-subset-Metric-Space
    ( metric-space-ℝ l)
    ( closed-subset-closed-interval-ℝ l [a,b])

complete-metric-space-closed-interval-ℝ :
  {l1 : Level} (l : Level) → closed-interval-ℝ l1 →
  Complete-Metric-Space (l1 ⊔ lsuc l) l
complete-metric-space-closed-interval-ℝ l [a,b] =
  complete-closed-subspace-Complete-Metric-Space
    ( complete-metric-space-ℝ l)
    ( closed-subset-closed-interval-ℝ l [a,b])

metric-space-unit-closed-interval-ℝ :
  (l : Level) → Metric-Space (lsuc l) l
metric-space-unit-closed-interval-ℝ l =
  metric-space-closed-interval-ℝ l unit-closed-interval-ℝ

complete-metric-space-unit-interval-ℝ :
  (l : Level) → Complete-Metric-Space (lsuc l) l
complete-metric-space-unit-interval-ℝ l =
  complete-metric-space-closed-interval-ℝ l unit-closed-interval-ℝ

Recent changes