Lipschitz-continuous functions between metric spaces (#1417)

This introduces the concept of *Lipschitz* functions between metric
spaces and proves that left/right multiplication of rational numbers is
Lipschitz.

More precisely, `metric-spaces.lipschitz-functions-metric-spaces`
introduces the following concepts and results:
  - Lipschitz constant for a function between metric spaces;
- Lipschitz functions between metric spaces (functions with some
Lipschitz constant);
  - constant functions are Lipschitz for all `α : ℚ⁺`;
- short functions are Lipschitz functions with Lipschitz constant equal
to 1;
  - Lipschitz functions are uniformly continuous;
  - the composition of Lipschitz maps is Lipschitz;
  - being a Lipschitz map is homotopy invariant;
  - Lipschitz maps preserve elements at bounded distance.

The metric space of Lipschitz functions is introduced in
`metric-spaces.metric-space-of-lipschitz-functions-metric-spaces`.

We also introduce a new concept in the `metric-spaces` module:
- `metric-spaces.elements-at-bounded-distance-metric-spaces`: the
equivalence relation of being at bounded distance in a metric space
(being in _some_ neighborhood).

Author: malarbol

src/elementary-number-theory/distance-rational-numbers.lagda.md

@@ -29,9 +29,6 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.transport-along-identifications
-
-open import metric-spaces.metric-space-of-rational-numbers
-open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods
 ```
 
 </details>
@@ -93,6 +90,30 @@ abstract
 
 ```agda
 abstract
+  left-distributive-abs-mul-dist-ℚ :
+    (p q r : ℚ) →
+    abs-ℚ p *ℚ⁰⁺ dist-ℚ q r ＝ dist-ℚ (p *ℚ q) (p *ℚ r)
+  left-distributive-abs-mul-dist-ℚ p q r =
+    equational-reasoning
+      abs-ℚ p *ℚ⁰⁺ dist-ℚ q r
+      ＝ abs-ℚ (p *ℚ (q -ℚ r))
+        by (inv (abs-mul-ℚ p (q -ℚ r)))
+      ＝ dist-ℚ (p *ℚ q) (p *ℚ r)
+        by ap abs-ℚ (left-distributive-mul-diff-ℚ p q r)
+
+  right-distributive-abs-mul-dist-ℚ :
+    (p q r : ℚ) →
+    dist-ℚ q r *ℚ⁰⁺ abs-ℚ p ＝ dist-ℚ (q *ℚ p) (r *ℚ p)
+  right-distributive-abs-mul-dist-ℚ p q r =
+    equational-reasoning
+      dist-ℚ q r *ℚ⁰⁺ abs-ℚ p
+      ＝ abs-ℚ p *ℚ⁰⁺ dist-ℚ q r
+        by commutative-mul-ℚ⁰⁺ (dist-ℚ q r) (abs-ℚ p)
+      ＝ dist-ℚ (p *ℚ q) (p *ℚ r)
+        by left-distributive-abs-mul-dist-ℚ p q r
+      ＝ dist-ℚ (q *ℚ p) (r *ℚ p)
+        by ap-binary dist-ℚ (commutative-mul-ℚ p q) (commutative-mul-ℚ p r)
+
   left-distributive-mul-dist-ℚ :
     (p : ℚ⁰⁺) (q r : ℚ) →
     p *ℚ⁰⁺ dist-ℚ q r ＝ dist-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r)
@@ -165,122 +186,6 @@ abstract
       ( inv-tr (λ s → le-ℚ s r) (distributive-neg-diff-ℚ p q) q-p<r)
 ```
 
-### Relationship to the metric space of rational numbers
-
-```agda
-abstract
-  leq-dist-neighborhood-leq-ℚ :
-    (ε : ℚ⁺) (p q : ℚ) →
-    neighborhood-leq-ℚ ε p q →
-    leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε)
-  leq-dist-neighborhood-leq-ℚ ε⁺@(ε , _) p q (H , K) =
-    leq-dist-leq-diff-ℚ
-      ( p)
-      ( q)
-      ( ε)
-      ( swap-right-diff-leq-ℚ p ε q (leq-transpose-right-add-ℚ p q ε K))
-      ( swap-right-diff-leq-ℚ q ε p (leq-transpose-right-add-ℚ q p ε H))
-
-  neighborhood-leq-leq-dist-ℚ :
-    (ε : ℚ⁺) (p q : ℚ) →
-    leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) →
-    neighborhood-leq-ℚ ε p q
-  neighborhood-leq-leq-dist-ℚ ε⁺@(ε , _) p q |p-q|≤ε =
-    ( leq-transpose-left-diff-ℚ
-      ( q)
-      ( ε)
-      ( p)
-      ( swap-right-diff-leq-ℚ
-        ( q)
-        ( p)
-        ( ε)
-        ( transitive-leq-ℚ
-          ( q -ℚ p)
-          ( rational-dist-ℚ p q)
-          ( ε)
-          ( |p-q|≤ε)
-          ( leq-reversed-diff-dist-ℚ p q)))) ,
-    ( leq-transpose-left-diff-ℚ
-      ( p)
-      ( ε)
-      ( q)
-      ( swap-right-diff-leq-ℚ
-        ( p)
-        ( q)
-        ( ε)
-        ( transitive-leq-ℚ
-          ( p -ℚ q)
-          ( rational-dist-ℚ p q)
-          ( ε)
-          ( |p-q|≤ε)
-          ( leq-diff-dist-ℚ p q))))
-
-leq-dist-iff-neighborhood-leq-ℚ :
-  (ε : ℚ⁺) (p q : ℚ) →
-  leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔
-  neighborhood-leq-ℚ ε p q
-pr1 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = neighborhood-leq-leq-dist-ℚ ε p q
-pr2 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = leq-dist-neighborhood-leq-ℚ ε p q
-```
-
-### Relationship to the metric space of rational numbers with open neighborhoods
-
-```agda
-abstract
-  le-dist-neighborhood-le-ℚ :
-    (ε : ℚ⁺) (p q : ℚ) →
-    neighborhood-le-ℚ ε p q →
-    le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε)
-  le-dist-neighborhood-le-ℚ ε⁺@(ε , _) p q (H , K) =
-    le-dist-le-diff-ℚ
-      ( p)
-      ( q)
-      ( ε)
-      ( swap-right-diff-le-ℚ p ε q (le-transpose-right-add-ℚ p q ε K))
-      ( swap-right-diff-le-ℚ q ε p (le-transpose-right-add-ℚ q p ε H))
-
-  neighborhood-le-le-dist-ℚ :
-    (ε : ℚ⁺) (p q : ℚ) →
-    le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) →
-    neighborhood-le-ℚ ε p q
-  neighborhood-le-le-dist-ℚ ε⁺@(ε , _) p q |p-q|<ε =
-    ( le-transpose-left-diff-ℚ
-      ( q)
-      ( ε)
-      ( p)
-      ( swap-right-diff-le-ℚ
-        ( q)
-        ( p)
-        ( ε)
-        ( concatenate-leq-le-ℚ
-          ( q -ℚ p)
-          ( rational-dist-ℚ p q)
-          ( ε)
-          ( leq-reversed-diff-dist-ℚ p q)
-          ( |p-q|<ε)))) ,
-    ( le-transpose-left-diff-ℚ
-      ( p)
-      ( ε)
-      ( q)
-      ( swap-right-diff-le-ℚ
-        ( p)
-        ( q)
-        ( ε)
-        ( concatenate-leq-le-ℚ
-          ( p -ℚ q)
-          ( rational-dist-ℚ p q)
-          ( ε)
-          ( leq-diff-dist-ℚ p q)
-          ( |p-q|<ε))))
-
-le-dist-iff-neighborhood-le-ℚ :
-  (ε : ℚ⁺) (p q : ℚ) →
-  le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔
-  neighborhood-le-ℚ ε p q
-pr1 (le-dist-iff-neighborhood-le-ℚ ε p q) = neighborhood-le-le-dist-ℚ ε p q
-pr2 (le-dist-iff-neighborhood-le-ℚ ε p q) = le-dist-neighborhood-le-ℚ ε p q
-```
-
 ### The distance between two rational numbers is the difference of their maximum and minimum
 
 ```agda

src/elementary-number-theory/inequality-integers.lagda.md

@@ -73,6 +73,13 @@ _≤-ℤ_ = leq-ℤ
 
 ## Properties
 
+### Zero is less than one
+
+```agda
+leq-zero-one-ℤ : leq-ℤ zero-ℤ one-ℤ
+leq-zero-one-ℤ = star
+```
+
 ### Inequality on the integers is reflexive, antisymmetric and transitive
 
 ```agda

src/elementary-number-theory/inequality-rational-numbers.lagda.md

@@ -84,6 +84,13 @@ _≤-ℚ_ = leq-ℚ
 
 ## Properties
 
+### Zero is less than one
+
+```agda
+leq-zero-one-ℚ : leq-ℚ zero-ℚ one-ℚ
+leq-zero-one-ℚ = leq-zero-one-ℤ
+```
+
 ### Inequality on the rational numbers is decidable
 
 ```agda
@@ -439,6 +446,17 @@ abstract
         ( leq-transpose-left-diff-ℚ p q r p-q≤r))
 ```
 
+### A rational number is lesser than its successor
+
+```agda
+succ-leq-ℚ : (p : ℚ) → leq-ℚ p (succ-ℚ p)
+succ-leq-ℚ p =
+  tr
+    ( λ x → leq-ℚ x (one-ℚ +ℚ p))
+    ( left-unit-law-add-ℚ p)
+    ( preserves-leq-left-add-ℚ p zero-ℚ one-ℚ leq-zero-one-ℚ)
+```
+
 ## See also
 
 - The decidable total order on the rational numbers is defined in

src/elementary-number-theory/nonnegative-rational-numbers.lagda.md

@@ -190,6 +190,26 @@ module _
         is-nonnegative-leq-zero-ℚ)
 ```
 
+### The successor of a nonnegative rational number is positive
+
+```agda
+abstract
+  is-positive-succ-is-nonnegative-ℚ :
+    (q : ℚ) → is-nonnegative-ℚ q → is-positive-ℚ (succ-ℚ q)
+  is-positive-succ-is-nonnegative-ℚ q H =
+    is-positive-le-zero-ℚ
+      ( succ-ℚ q)
+      ( concatenate-leq-le-ℚ
+        ( zero-ℚ)
+        ( q)
+        ( succ-ℚ q)
+        ( leq-zero-is-nonnegative-ℚ q H)
+        ( le-left-add-rational-ℚ⁺ q one-ℚ⁺))
+
+positive-succ-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁺
+positive-succ-ℚ⁰⁺ (q , H) = (succ-ℚ q , is-positive-succ-is-nonnegative-ℚ q H)
+```
+
 ### The product of two nonnegative rational numbers is nonnegative
 
 ```agda

src/elementary-number-theory/positive-rational-numbers.lagda.md

@@ -177,6 +177,14 @@ one-ℚ⁺ : ℚ⁺
 one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ)
 ```
 
+### The type of positive rational numbers is inhabited
+
+```agda
+abstract
+  is-inhabited-ℚ⁺ : ║ ℚ⁺ ║₋₁
+  is-inhabited-ℚ⁺ = unit-trunc-Prop one-ℚ⁺
+```
+
 ### The rational image of a positive natural number is positive
 
 ```agda

src/metric-spaces.lagda.md

@@ -59,6 +59,7 @@ open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.convergent-sequences-metric-spaces public
 open import metric-spaces.dependent-products-metric-spaces public
 open import metric-spaces.discrete-premetric-structures public
+open import metric-spaces.elements-at-bounded-distance-metric-spaces public
 open import metric-spaces.equality-of-metric-spaces public
 open import metric-spaces.equality-of-premetric-spaces public
 open import metric-spaces.extensional-premetric-structures public
@@ -73,13 +74,15 @@ open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces publi
 open import metric-spaces.limits-of-sequences-metric-spaces public
 open import metric-spaces.limits-of-sequences-premetric-spaces public
 open import metric-spaces.limits-of-sequences-pseudometric-spaces public
+open import metric-spaces.lipschitz-functions-metric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-sequences-metric-spaces public
 open import metric-spaces.metric-space-of-functions-metric-spaces public
 open import metric-spaces.metric-space-of-isometries-metric-spaces public
+open import metric-spaces.metric-space-of-lipschitz-functions-metric-spaces public
 open import metric-spaces.metric-space-of-rational-numbers public
 open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods public
 open import metric-spaces.metric-space-of-short-functions-metric-spaces public