Continuous maps between metric spaces

Content created by Fredrik Bakke and Louis Wasserman.

Created on 2026-01-01.
Last modified on 2026-01-01.

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

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.inhabited-subtypes
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import metric-spaces.limits-of-maps-metric-spaces
open import metric-spaces.maps-metric-spaces
open import metric-spaces.metric-spaces

Idea

A map f between metric spaces X and Y is continuous at a point x if f x is the limit of f at x. I.e., there exists a function m : ℚ⁺ → ℚ⁺ such that whenever x' is in an m ε-neighborhood of x, f x' is in an ε-neighborhood of f x. In this case, m is called a modulus of continuity of f at x.

Definitions

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : map-Metric-Space X Y)
  (x : type-Metric-Space X)
  where

  is-continuous-at-point-prop-map-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4)
  is-continuous-at-point-prop-map-Metric-Space =
    is-point-limit-prop-map-Metric-Space X Y f x (f x)

  is-continuous-at-point-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4)
  is-continuous-at-point-map-Metric-Space =
    is-point-limit-map-Metric-Space X Y f x (f x)

  is-modulus-of-continuity-at-point-prop-map-Metric-Space :
    (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4)
  is-modulus-of-continuity-at-point-prop-map-Metric-Space =
    is-modulus-of-point-limit-prop-map-Metric-Space X Y f x (f x)

  is-modulus-of-continuity-at-point-map-Metric-Space :
    (ℚ⁺ → ℚ⁺) → UU (l1 ⊔ l2 ⊔ l4)
  is-modulus-of-continuity-at-point-map-Metric-Space =
    is-modulus-of-point-limit-map-Metric-Space X Y f x (f x)

  modulus-of-continuity-at-point-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4)
  modulus-of-continuity-at-point-map-Metric-Space =
    type-subtype
      is-modulus-of-continuity-at-point-prop-map-Metric-Space

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : map-Metric-Space X Y)
  where

  is-pointwise-continuous-prop-map-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4)
  is-pointwise-continuous-prop-map-Metric-Space =
    Π-Prop
      ( type-Metric-Space X)
      ( is-continuous-at-point-prop-map-Metric-Space X Y f)

  is-pointwise-continuous-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4)
  is-pointwise-continuous-map-Metric-Space =
    type-Prop is-pointwise-continuous-prop-map-Metric-Space

Recent changes