The metric space of 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-cauchy-approximations-in-a-metric-space where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.universe-levels

open import metric-spaces.cauchy-approximations-metric-spaces
open import metric-spaces.dependent-products-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

The type of Cauchy approximations in a metric space A inherits the metric substructure of the constant product structure over A.

This is the metric space of 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-cauchy-approximations-Metric-Space : Metric-Space (l1 ⊔ l2) l2
  metric-space-cauchy-approximations-Metric-Space =
    subspace-Metric-Space
      ( Π-Metric-Space ℚ⁺ (λ _ → A))
      ( is-cauchy-approximation-prop-Metric-Space A)

Recent changes