Complete metric spaces

Content created by Fredrik Bakke and malarbol.

Created on 2024-09-28.
Last modified on 2024-09-28.

module metric-spaces.complete-metric-spaces where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import metric-spaces.cauchy-approximations-metric-spaces
open import metric-spaces.convergent-cauchy-approximations-metric-spaces
open import metric-spaces.metric-spaces

Idea

A metric space is complete if all its Cauchy approximations are convergent.

Definitions

The property of being a complete metric space

module _
  {l1 l2 : Level} (A : Metric-Space l1 l2)
  where

  is-complete-prop-Metric-Space : Prop (l1 ⊔ l2)
  is-complete-prop-Metric-Space =
    Π-Prop
      ( cauchy-approximation-Metric-Space A)
      ( is-convergent-prop-cauchy-approximation-Metric-Space A)

  is-complete-Metric-Space : UU (l1 ⊔ l2)
  is-complete-Metric-Space = type-Prop is-complete-prop-Metric-Space

  is-prop-is-complete-Metric-Space : is-prop is-complete-Metric-Space
  is-prop-is-complete-Metric-Space =
    is-prop-type-Prop is-complete-prop-Metric-Space

The type of complete metric spaces

module _
  (l1 l2 : Level)
  where

  Complete-Metric-Space : UU (lsuc l1 ⊔ lsuc l2)
  Complete-Metric-Space =
    type-subtype (is-complete-prop-Metric-Space {l1} {l2})

module _
  {l1 l2 : Level}
  (A : Complete-Metric-Space l1 l2)
  where

  metric-space-Complete-Metric-Space : Metric-Space l1 l2
  metric-space-Complete-Metric-Space = pr1 A

  type-Complete-Metric-Space : UU l1
  type-Complete-Metric-Space =
    type-Metric-Space metric-space-Complete-Metric-Space

  is-complete-metric-space-Complete-Metric-Space :
    is-complete-Metric-Space metric-space-Complete-Metric-Space
  is-complete-metric-space-Complete-Metric-Space = pr2 A

Recent changes