The metric space of convergent cauchy approximations in a metric space

Content created by Fredrik Bakke and malarbol.

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

module metric-spaces.metric-space-of-convergent-cauchy-approximations-in-a-metric-space where
Imports 
open import foundation.universe-levels

open import metric-spaces.convergent-cauchy-approximations-metric-spaces
open import metric-spaces.metric-space-of-cauchy-approximations-in-a-metric-space
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

The type of convergent Cauchy approximations in a metric space inherits the metric substructure of the metric space of Cauchy approximations. This is the metric space of convergent Cauchy approximations in a metric space.

Definitions

The metric space of cauchy approximations in a metric space

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

  metric-space-convergent-cauchy-approximations-Metric-Space :
    Metric-Space (l1 ⊔ l2) l2
  metric-space-convergent-cauchy-approximations-Metric-Space =
    subspace-Metric-Space
      ( metric-space-cauchy-approximations-Metric-Space A)
      ( is-convergent-prop-cauchy-approximation-Metric-Space A)

Recent changes