Uniformly continuous endomaps on the real numbers

Content created by Fredrik Bakke and Louis Wasserman.

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

{-# OPTIONS --lossy-unification #-}

module real-numbers.uniformly-continuous-endomaps-real-numbers where
Imports 
open import foundation.universe-levels

open import metric-spaces.uniformly-continuous-maps-metric-spaces

open import real-numbers.dedekind-real-numbers
open import real-numbers.metric-space-of-real-numbers

Idea

A uniformly continuous endomap on the real numbers is a function f : ℝ → ℝ such that there exists a modulus μ : ℚ⁺ → ℚ⁺, called a modulus of uniform continuity, such that for all x y : ℝ within a μ ε-neighborhood of each other, f x and f y are within an ε-neighborhood. In other words, it is a uniformly continuous map from the metric space of real numbers to itself.

Definition

uniformly-continuous-endomap-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
uniformly-continuous-endomap-ℝ l1 l2 =
  uniformly-continuous-map-Metric-Space
    ( metric-space-ℝ l1)
    ( metric-space-ℝ l2)

comp-uniformly-continuous-endomap-ℝ :
  {l1 l2 l3 : Level} →
  uniformly-continuous-endomap-ℝ l2 l3 →
  uniformly-continuous-endomap-ℝ l1 l2 →
  uniformly-continuous-endomap-ℝ l1 l3
comp-uniformly-continuous-endomap-ℝ {l1} {l2} {l3} =
  comp-uniformly-continuous-map-Metric-Space
    ( metric-space-ℝ l1)
    ( metric-space-ℝ l2)
    ( metric-space-ℝ l3)

map-uniformly-continuous-endomap-ℝ :
  {l1 l2 : Level} → uniformly-continuous-endomap-ℝ l1 l2 → ℝ l1 → ℝ l2
map-uniformly-continuous-endomap-ℝ {l1} {l2} =
  map-uniformly-continuous-map-Metric-Space
    ( metric-space-ℝ l1)
    ( metric-space-ℝ l2)

Recent changes