Continuity of functions between metric spaces

src/metric-spaces.lagda.md

@@ -53,6 +53,7 @@ open import metric-spaces.cauchy-sequences-complete-metric-spaces public
 open import metric-spaces.cauchy-sequences-metric-spaces public
 open import metric-spaces.closed-premetric-structures public
 open import metric-spaces.complete-metric-spaces public
+open import metric-spaces.continuous-functions-metric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.dependent-products-metric-spaces public
 open import metric-spaces.discrete-premetric-structures public
@@ -89,6 +90,7 @@ open import metric-spaces.short-functions-premetric-spaces public
 open import metric-spaces.subspaces-metric-spaces public
 open import metric-spaces.symmetric-premetric-structures public
 open import metric-spaces.triangular-premetric-structures public
+open import metric-spaces.uniformly-continuous-functions-metric-spaces public
 ```
 
 ## References

src/metric-spaces/continuous-functions-metric-spaces.lagda.md

@@ -0,0 +1,70 @@
+# Continuous functions between metric spaces
+
+```agda
+module metric-spaces.continuous-functions-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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.functions-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) `f` between
+[metric spaces](metric-spaces.metric-spaces.md) `X` and `Y` is
+{{#concept "continuous" WDID=Q170058 WD="continuous function"}} at a point `x`
+if 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`. `m` is
+called a modulus of continuity of `f` at `x`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
+  (f : map-type-Metric-Space X Y)
+  where
+
+  modulus-of-continuity-at-point-Metric-Space-Prop :
+    (x : type-Metric-Space X) → (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4)
+  modulus-of-continuity-at-point-Metric-Space-Prop x m =
+    Π-Prop
+      ( ℚ⁺)
+      ( λ ε →
+        Π-Prop
+          ( type-Metric-Space X)
+          ( λ x' →
+            structure-Metric-Space X (m ε) x x' ⇒
+            structure-Metric-Space Y ε (f x) (f x')))
+
+  modulus-of-continuity-at-point-Metric-Space :
+    (x : type-Metric-Space X) → UU (l1 ⊔ l2 ⊔ l4)
+  modulus-of-continuity-at-point-Metric-Space x =
+    type-subtype (modulus-of-continuity-at-point-Metric-Space-Prop x)
+
+  continuous-at-point-Metric-Space-Prop :
+    (x : type-Metric-Space X) → Prop (l1 ⊔ l2 ⊔ l4)
+  continuous-at-point-Metric-Space-Prop x =
+    is-inhabited-subtype-Prop
+      (modulus-of-continuity-at-point-Metric-Space-Prop x)
+
+  is-continuous-at-point-Metric-Space :
+    (x : type-Metric-Space X) → UU (l1 ⊔ l2 ⊔ l4)
+  is-continuous-at-point-Metric-Space x =
+    type-Prop (continuous-at-point-Metric-Space-Prop x)
+```

src/metric-spaces/isometries-metric-spaces.lagda.md

@@ -30,6 +30,7 @@ open import foundation.universe-levels
 open import metric-spaces.functions-metric-spaces
 open import metric-spaces.isometries-premetric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
 ```
 
 </details>
@@ -344,11 +345,31 @@ module _
   where
 
   is-emb-map-isometry-Metric-Space :
-      (f : isometry-Metric-Space A B) → is-emb (map-isometry-Metric-Space A B f)
+    (f : isometry-Metric-Space A B) → is-emb (map-isometry-Metric-Space A B f)
   is-emb-map-isometry-Metric-Space =
     is-emb-map-isometry-is-extensional-Premetric-Space
       ( premetric-Metric-Space A)
       ( premetric-Metric-Space B)
       ( is-extensional-structure-Metric-Space A)
       ( is-extensional-structure-Metric-Space B)
 ```
+
+### Any isometry between metric spaces is uniformly continuous
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l3 l4)
+  where
+
+  is-uniformly-continuous-map-isometry-Metric-Space :
+    (f : isometry-Metric-Space A B) →
+    is-uniformly-continuous-map-Metric-Space A B
+      (map-isometry-Metric-Space A B f)
+  is-uniformly-continuous-map-isometry-Metric-Space f =
+    intro-exists
+      ( id)
+      ( λ x ε x' →
+        forward-implication
+          ( is-isometry-map-isometry-Metric-Space A B f ε x x'))
+```

src/metric-spaces/short-functions-metric-spaces.lagda.md

@@ -12,6 +12,7 @@ open import elementary-number-theory.positive-rational-numbers
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
+open import foundation.existential-quantification
 open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.homotopies
@@ -27,6 +28,7 @@ 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-premetric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
 ```
 
 </details>
@@ -323,6 +325,20 @@ module _
         ( is-emb-inclusion-subtype (is-isometry-prop-Metric-Space A B)))
 ```
 
+### Short maps are uniformly continuous
+
+```agda
+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 : map-type-Metric-Space A B) → is-short-function-Metric-Space A B f →
+    is-uniformly-continuous-map-Metric-Space A B f
+  is-uniformly-continuous-is-short-function-Metric-Space f H =
+    intro-exists id (λ x ε → H ε x)
+```
+
 ## See also
 
 - The

src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md

@@ -0,0 +1,111 @@
+# Uniformly continuous functions between metric spaces
+
+```agda
+module metric-spaces.uniformly-continuous-functions-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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.inhabited-subtypes
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.continuous-functions-metric-spaces
+open import metric-spaces.functions-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [function](metric-spaces.functions-metric-spaces.md) `f` between
+[metric spaces](metric-spaces.metric-spaces.md) `X` and `Y` is
+{{#concept "uniformly continuous" WDID=Q170058 WD="continuous function"}} 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
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
+  (f : map-type-Metric-Space X Y)
+  where
+
+  modulus-of-uniform-continuity-Metric-Space-Prop :
+    (ℚ⁺ → ℚ⁺) → Prop (l1 ⊔ l2 ⊔ l4)
+  modulus-of-uniform-continuity-Metric-Space-Prop m =
+    Π-Prop
+      ( type-Metric-Space X)
+      ( λ x → modulus-of-continuity-at-point-Metric-Space-Prop X Y f x m)
+
+  uniformly-continuous-Metric-Space-Prop : Prop (l1 ⊔ l2 ⊔ l4)
+  uniformly-continuous-Metric-Space-Prop =
+    is-inhabited-subtype-Prop modulus-of-uniform-continuity-Metric-Space-Prop
+
+  is-uniformly-continuous-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4)
+  is-uniformly-continuous-map-Metric-Space =
+    type-Prop uniformly-continuous-Metric-Space-Prop
+
+  is-continuous-at-point-is-uniformly-continuous-map-Metric-Space :
+    is-uniformly-continuous-map-Metric-Space → (x : type-Metric-Space X) →
+    is-continuous-at-point-Metric-Space X Y f x
+  is-continuous-at-point-is-uniformly-continuous-map-Metric-Space H x =
+    do
+      m , is-modulus-uniform-m ← H
+      intro-exists m (is-modulus-uniform-m x)
+    where
+      open do-syntax-trunc-Prop (continuous-at-point-Metric-Space-Prop X Y f x)
+```
+
+## Properties
+
+### The identity function is uniformly continuous
+
+```agda
+module _
+  {l1 l2 : Level} (X : Metric-Space l1 l2)
+  where
+
+  uniformly-continuous-id-Metric-Space :
+    is-uniformly-continuous-map-Metric-Space X X id
+  uniformly-continuous-id-Metric-Space = intro-exists id (λ _ _ _ → id)
+```
+
+### The composition of uniformly continuous functions is uniformly continuous
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) (Z : Metric-Space l5 l6)
+  (f : map-type-Metric-Space Y Z) (g : map-type-Metric-Space X Y)
+  where
+
+  uniformly-continuous-comp-uniformly-continuous-Metric-Space :
+    is-uniformly-continuous-map-Metric-Space Y Z f →
+    is-uniformly-continuous-map-Metric-Space X Y g →
+    is-uniformly-continuous-map-Metric-Space X Z (f ∘ g)
+  uniformly-continuous-comp-uniformly-continuous-Metric-Space H K =
+    do
+      mf , is-modulus-uniform-mf ← H
+      mg , is-modulus-uniform-mg ← K
+      intro-exists
+        ( mg ∘ mf)
+        ( λ x ε x' →
+          is-modulus-uniform-mf (g x) ε (g x') ∘
+          is-modulus-uniform-mg x (mf ε) x')
+    where
+      open
+        do-syntax-trunc-Prop
+          ( uniformly-continuous-Metric-Space-Prop X Z (f ∘ g))
+```