Metric spaces

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

@@ -13,6 +13,8 @@ open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.additive-group-of-rational-numbers
 open import elementary-number-theory.cross-multiplication-difference-integer-fractions
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integer-fractions
@@ -29,11 +31,13 @@ open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.reduced-integer-fractions
 open import elementary-number-theory.strict-inequality-rational-numbers
 
+open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositions
 open import foundation.sets
@@ -175,6 +179,18 @@ module _
       is-positive-eq-ℤ (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))
 ```
 
+### The difference of a rational number with a lesser rational number is positive
+
+```agda
+is-positive-diff-le-ℚ : (x y : ℚ) → le-ℚ x y → is-positive-ℚ (y -ℚ x)
+is-positive-diff-le-ℚ x y H =
+  is-positive-le-zero-ℚ
+    ( y -ℚ x)
+    ( backward-implication
+      ( iff-translate-diff-le-zero-ℚ x y)
+      ( H))
+```
+
 ### A nonzero rational number or its negative is positive
 
 ```agda
@@ -432,4 +448,86 @@ module _
         ( le-zero-is-positive-ℚ
           ( rational-ℚ⁺ x)
           ( is-positive-rational-ℚ⁺ x)))
+
+module _
+  (x y : ℚ⁺) (H : le-ℚ⁺ x y)
+  where
+
+  le-diff-ℚ⁺ : ℚ⁺
+  pr1 le-diff-ℚ⁺ = (rational-ℚ⁺ y) -ℚ (rational-ℚ⁺ x)
+  pr2 le-diff-ℚ⁺ =
+    is-positive-le-zero-ℚ
+      ( (rational-ℚ⁺ y) -ℚ (rational-ℚ⁺ x))
+      ( backward-implication
+        ( iff-translate-diff-le-zero-ℚ
+          ( rational-ℚ⁺ x)
+          ( rational-ℚ⁺ y))
+        ( ( H)))
+
+  left-diff-law-add-ℚ⁺ : le-diff-ℚ⁺ +ℚ⁺ x ＝ y
+  left-diff-law-add-ℚ⁺ =
+    eq-ℚ⁺
+      ( ( associative-add-ℚ
+          ( rational-ℚ⁺ y)
+          ( neg-ℚ (rational-ℚ⁺ x))
+          ( rational-ℚ⁺ x)) ∙
+        ( ( ap
+            ( (rational-ℚ⁺ y) +ℚ_)
+            ( left-inverse-law-add-ℚ (rational-ℚ⁺ x))) ∙
+        ( right-unit-law-add-ℚ (rational-ℚ⁺ y))))
+
+  right-diff-law-add-ℚ⁺ : x +ℚ⁺ le-diff-ℚ⁺ ＝ y
+  right-diff-law-add-ℚ⁺ =
+    ( eq-ℚ⁺
+      ( commutative-add-ℚ
+        ( rational-ℚ⁺ x)
+        ( rational-ℚ⁺ le-diff-ℚ⁺))) ∙
+    ( left-diff-law-add-ℚ⁺)
+```
+
+### The positive mediant between zero and a positive rational numbers
+
+```agda
+mediant-zero-ℚ⁺ : ℚ⁺ → ℚ⁺
+mediant-zero-ℚ⁺ x =
+  ( mediant-ℚ zero-ℚ (rational-ℚ⁺ x) ,
+    is-positive-le-zero-ℚ
+      ( mediant-ℚ zero-ℚ (rational-ℚ⁺ x))
+      ( le-left-mediant-ℚ
+        ( zero-ℚ)
+        ( rational-ℚ⁺ x)
+        ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))))
+
+le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
+le-mediant-zero-ℚ⁺ x =
+  ( le-right-mediant-ℚ
+    ( zero-ℚ)
+    ( rational-ℚ⁺ x)
+    ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x)))
+```
+
+### The addition with a positive rational number is an increasing map
+
+```agda
+le-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x ((rational-ℚ⁺ d) +ℚ x)
+le-left-add-rational-ℚ⁺ x d =
+  concatenate-leq-le-ℚ
+    ( x)
+    ( zero-ℚ +ℚ x)
+    ( (rational-ℚ⁺ d) +ℚ x)
+    ( inv-tr (leq-ℚ x) (left-unit-law-add-ℚ x) (refl-leq-ℚ x))
+    ( preserves-le-left-add-ℚ
+      ( x)
+      ( zero-ℚ)
+      ( rational-ℚ⁺ d)
+      ( le-zero-is-positive-ℚ
+        ( rational-ℚ⁺ d)
+        ( is-positive-rational-ℚ⁺ d)))
+
+le-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x (x +ℚ (rational-ℚ⁺ d))
+le-right-add-rational-ℚ⁺ x d =
+  inv-tr
+    ( le-ℚ x)
+    ( commutative-add-ℚ x (rational-ℚ⁺ d))
+    ( le-left-add-rational-ℚ⁺ x d)
 ```

src/metric-spaces.lagda.md

@@ -0,0 +1,17 @@
+# Metric spaces
+
+```agda
+module metric-spaces where
+
+open import metric-spaces.cauchy-sequences-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.functions-metric-spaces public
+open import metric-spaces.metric-space-of-rational-numbers public
+open import metric-spaces.metric-spaces public
+open import metric-spaces.neighbourhood-relations public
+open import metric-spaces.pointwise-continuity-functions-metric-spaces public
+open import metric-spaces.sequences-metric-spaces public
+open import metric-spaces.subsets-metric-spaces public
+open import metric-spaces.uniform-continuity-functions-metric-spaces public
+```

src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md

@@ -0,0 +1,119 @@
+# Cauchy sequences in metric spaces
+
+```agda
+module metric-spaces.cauchy-sequences-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import metric-spaces.convergent-sequences-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.neighbourhood-relations
+open import metric-spaces.sequences-metric-spaces
+```
+
+</details>
+
+## Idea
+
+Cauchy sequences in metric spaces are sequences that satisfy the Cauchy
+criterion.
+
+## Definitions
+
+### Cauchy sequences in metric spaces
+
+```agda
+module _
+  {l : Level} (M : Metric-Space l) (u : Sequence-Metric-Space M)
+  where
+
+  is-modulus-cauchy-prop-Sequence-Metric-Space : (d : ℚ⁺) (N : ℕ) → Prop l
+  is-modulus-cauchy-prop-Sequence-Metric-Space d N =
+    Π-Prop
+      ( ℕ)
+      ( λ (n : ℕ) →
+        ( Π-Prop
+          ( ℕ)
+          ( λ (m : ℕ) →
+            hom-Prop
+              ( leq-ℕ-Prop N n)
+              ( hom-Prop
+                ( leq-ℕ-Prop N m)
+                ( neighbourhood-Metric-Space M d (u n) (u m))))))
+
+  is-modulus-cauchy-Sequence-Metric-Space : (d : ℚ⁺) (N : ℕ) → UU l
+  is-modulus-cauchy-Sequence-Metric-Space d N =
+    type-Prop (is-modulus-cauchy-prop-Sequence-Metric-Space d N)
+
+  is-cauchy-Sequence-Metric-Space : UU l
+  is-cauchy-Sequence-Metric-Space =
+    (d : ℚ⁺) → Σ ℕ (is-modulus-cauchy-Sequence-Metric-Space d)
+```
+
+### Convergent sequences in metric spaces are Cauchy sequences
+
+```agda
+module _
+  {l : Level} (M : Metric-Space l) (u : Sequence-Metric-Space M)
+  where
+
+  is-cauchy-is-convergent-Sequence-Metric-Space :
+    is-convergent-Sequence-Metric-Space M u →
+    is-cauchy-Sequence-Metric-Space M u
+  is-cauchy-is-convergent-Sequence-Metric-Space (x , H) d = (N , α)
+    where
+      d₂ : ℚ⁺
+      d₂ = mediant-zero-ℚ⁺ d
+
+      d₁ : ℚ⁺
+      d₁ = le-diff-ℚ⁺ d₂ d (le-mediant-zero-ℚ⁺ d)
+
+      Np : ℕ
+      Np = modulus-limit-Sequence-Metric-Space M u x H d₁
+
+      Nq : ℕ
+      Nq = modulus-limit-Sequence-Metric-Space M u x H d₂
+
+      N : ℕ
+      N = max-ℕ Np Nq
+
+      α : is-modulus-cauchy-Sequence-Metric-Space M u d N
+      α p q I J =
+        tr
+          ( λ d' → is-in-neighbourhood-Metric-Space M d' (u p) (u q))
+          ( left-diff-law-add-ℚ⁺ d₂ d (le-mediant-zero-ℚ⁺ d))
+          ( is-triangular-neighbourhood-Metric-Space M
+            ( u p)
+            ( x)
+            ( u q)
+            ( d₁)
+            ( d₂)
+            ( γ)
+            ( is-symmetric-neighbourhood-Metric-Space M d₁ x (u p) β))
+        where
+          β : is-in-neighbourhood-Metric-Space M d₁ x (u p)
+          β =
+            is-modulus-modulus-limit-Sequence-Metric-Space M u x H d₁ p
+              ( transitive-leq-ℕ Np N p I
+                ( leq-left-leq-max-ℕ N Np Nq (refl-leq-ℕ N)))
+
+          γ : is-in-neighbourhood-Metric-Space M d₂ x (u q)
+          γ =
+            is-modulus-modulus-limit-Sequence-Metric-Space M u x H d₂ q
+              ( transitive-leq-ℕ Nq N q J
+                ( leq-right-leq-max-ℕ N Np Nq (refl-leq-ℕ N)))
+```