Uniformly continuous functions between metric spaces
Content created by Louis Wasserman and malarbol.
Created on 2025-03-30.
Last modified on 2025-08-18.
module metric-spaces.uniformly-continuous-functions-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.function-types open import foundation.functoriality-dependent-pair-types 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 logic.functoriality-existential-quantification open import metric-spaces.continuous-functions-metric-spaces open import metric-spaces.functions-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.short-functions-metric-spaces
Idea
A function f
between
metric spaces X
and Y
is
uniformly continuous¶
if there exists a function m : ℚ⁺ → ℚ⁺
such that for any x : X
, whenever
x'
is in an m ε
-neighborhood of x
, f x'
is in an ε
-neighborhood of
f x
. The function m
is called a modulus of uniform continuity of f
.
Definitions
The property of being a uniformly continuous function
module _ {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (f : type-function-Metric-Space X Y) where is-modulus-of-uniform-continuity-prop-function-Metric-Space : (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4) is-modulus-of-uniform-continuity-prop-function-Metric-Space m = Π-Prop ( type-Metric-Space X) ( λ x → is-modulus-of-continuity-at-point-prop-function-Metric-Space X Y f x m) modulus-of-uniform-continuity-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) modulus-of-uniform-continuity-function-Metric-Space = type-subtype is-modulus-of-uniform-continuity-prop-function-Metric-Space is-uniformly-continuous-prop-function-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) is-uniformly-continuous-prop-function-Metric-Space = is-inhabited-subtype-Prop is-modulus-of-uniform-continuity-prop-function-Metric-Space is-uniformly-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) is-uniformly-continuous-function-Metric-Space = type-Prop is-uniformly-continuous-prop-function-Metric-Space
The type of uniformly continuous functions between metric spaces
module _ {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) where uniformly-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) uniformly-continuous-function-Metric-Space = type-subtype (is-uniformly-continuous-prop-function-Metric-Space X Y) map-uniformly-continuous-function-Metric-Space : uniformly-continuous-function-Metric-Space → type-function-Metric-Space X Y map-uniformly-continuous-function-Metric-Space = pr1 is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space : (f : uniformly-continuous-function-Metric-Space) → is-uniformly-continuous-function-Metric-Space ( X) ( Y) ( map-uniformly-continuous-function-Metric-Space f) is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space = pr2
Properties
Uniformly continuous functions are continuous everywhere
module _ {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (f : type-function-Metric-Space X Y) where is-continuous-at-point-is-uniformly-continuous-function-Metric-Space : is-uniformly-continuous-function-Metric-Space X Y f → (x : type-Metric-Space X) → is-continuous-at-point-function-Metric-Space X Y f x is-continuous-at-point-is-uniformly-continuous-function-Metric-Space H x = elim-exists ( is-continuous-at-point-prop-function-Metric-Space X Y f x) ( λ m K → intro-exists m (K x)) ( H)
The identity function is uniformly continuous
module _ {l1 l2 : Level} (X : Metric-Space l1 l2) where is-uniformly-continuous-id-Metric-Space : is-uniformly-continuous-function-Metric-Space X X id is-uniformly-continuous-id-Metric-Space = intro-exists id (λ _ _ _ → id)
The composition of uniformly continuous functions is uniformly continuous
module _ {l1 l2 l3 l4 l5 l6 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (Z : Metric-Space l5 l6) where is-uniformly-continuous-comp-function-Metric-Space : (g : type-function-Metric-Space Y Z) → (f : type-function-Metric-Space X Y) → is-uniformly-continuous-function-Metric-Space Y Z g → is-uniformly-continuous-function-Metric-Space X Y f → is-uniformly-continuous-function-Metric-Space X Z (g ∘ f) is-uniformly-continuous-comp-function-Metric-Space g f H K = let open do-syntax-trunc-Prop ( is-uniformly-continuous-prop-function-Metric-Space X Z (g ∘ f)) in do mg , is-modulus-uniform-mg ← H mf , is-modulus-uniform-mf ← K intro-exists ( mf ∘ mg) ( λ x ε x' → is-modulus-uniform-mg (f x) ε (f x') ∘ is-modulus-uniform-mf x (mg ε) x') comp-uniformly-continuous-function-Metric-Space : uniformly-continuous-function-Metric-Space Y Z → uniformly-continuous-function-Metric-Space X Y → uniformly-continuous-function-Metric-Space X Z comp-uniformly-continuous-function-Metric-Space g f = ( map-uniformly-continuous-function-Metric-Space Y Z g ∘ map-uniformly-continuous-function-Metric-Space X Y f) , ( is-uniformly-continuous-comp-function-Metric-Space ( map-uniformly-continuous-function-Metric-Space Y Z g) ( map-uniformly-continuous-function-Metric-Space X Y f) ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space ( Y) ( Z) ( g)) ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space ( X) ( Y) ( f)))
Short maps are uniformly continuous
module _ {l1 l2 l3 l4 : Level} (A : Metric-Space l1 l2) (B : Metric-Space l3 l4) where is-uniformly-continuous-is-short-function-Metric-Space : (f : type-function-Metric-Space A B) → is-short-function-Metric-Space A B f → is-uniformly-continuous-function-Metric-Space A B f is-uniformly-continuous-is-short-function-Metric-Space f H = intro-exists id (λ x d → H d x) uniformly-continuous-short-function-Metric-Space : short-function-Metric-Space A B → uniformly-continuous-function-Metric-Space A B uniformly-continuous-short-function-Metric-Space = tot is-uniformly-continuous-is-short-function-Metric-Space
Isometries are uniformly continuous
module _ {l1 l2 l3 l4 : Level} (A : Metric-Space l1 l2) (B : Metric-Space l3 l4) where is-uniformly-continuous-is-isometry-Metric-Space : (f : type-function-Metric-Space A B) → is-isometry-Metric-Space A B f → is-uniformly-continuous-function-Metric-Space A B f is-uniformly-continuous-is-isometry-Metric-Space f = is-uniformly-continuous-is-short-function-Metric-Space A B f ∘ is-short-is-isometry-Metric-Space A B f uniformly-continuous-isometry-Metric-Space : isometry-Metric-Space A B → uniformly-continuous-function-Metric-Space A B uniformly-continuous-isometry-Metric-Space = tot is-uniformly-continuous-is-isometry-Metric-Space
External links
- Uniform continuity at Wikidata
Recent changes
- 2025-08-18. malarbol and Louis Wasserman. Refactor metric spaces (#1450).
- 2025-05-19. malarbol. Lipschitz-continuous functions between metric spaces (#1417).
- 2025-03-30. Louis Wasserman. Continuity of functions between metric spaces (#1375).