Limits of sequences in metric spaces (#1378)

This PR formalizes a few definitions and results about limits in
(pre|pseudo|)metric spaces.
It introduces the following modules:

- `metric-spaces.sequences-premetric-spaces`:
  - sequences in premetric spaces.

- `metric-spaces.limits-sequences-premetric-spaces`:
  - limits of sequences in premetric spaces;
  - short maps preserve limits.

- `metric-spaces.sequences-pseudometric-spaces`:
  - sequences in pseudometric spaces.

- `metric-spaces.limits-sequences-pseudometric-spaces`:
  - limits of sequences in pseudometric spaces;
- indistinguishability of limits of a sequence in a pseudometric space.

- `metric-spaces.sequences-metric-spaces`:
  - the metric space of sequences in a metric space.

- ` metric-spaces.limits-sequences-metric-spaces`:
  - limits of sequences in metric spaces;
  - unicity of the limit of a sequence in a metric space.

- `metric-spaces.convergent-sequences-metric-spaces`:
  - sequences in a metric space that have a limit;
  - short maps between metric spaces preserve convergent sequences.

-
`metric-spaces.metric-space-of-convergent-sequences-in-a-metric-space`:
  - the metric space of convergent sequences in a metric space.

Author: malarbol

src/metric-spaces.lagda.md

@@ -56,6 +56,7 @@ open import metric-spaces.complete-metric-spaces public
 open import metric-spaces.continuous-functions-metric-spaces public
 open import metric-spaces.continuous-functions-premetric-spaces public
 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.equality-of-metric-spaces public
@@ -68,11 +69,15 @@ open import metric-spaces.induced-premetric-structures-on-preimages public
 open import metric-spaces.isometric-equivalences-premetric-spaces public
 open import metric-spaces.isometries-metric-spaces public
 open import metric-spaces.isometries-premetric-spaces public
-open import metric-spaces.limits-of-cauchy-approximations-in-premetric-spaces public
+open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces public
+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.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-rational-numbers public
 open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods public
 open import metric-spaces.metric-spaces public
@@ -89,6 +94,9 @@ open import metric-spaces.pseudometric-structures public
 open import metric-spaces.reflexive-premetric-structures public
 open import metric-spaces.saturated-complete-metric-spaces public
 open import metric-spaces.saturated-metric-spaces public
+open import metric-spaces.sequences-metric-spaces public
+open import metric-spaces.sequences-premetric-spaces public
+open import metric-spaces.sequences-pseudometric-spaces public
 open import metric-spaces.short-functions-metric-spaces public
 open import metric-spaces.short-functions-premetric-spaces public
 open import metric-spaces.subspaces-metric-spaces public

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

@@ -19,7 +19,7 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import metric-spaces.cauchy-approximations-premetric-spaces
-open import metric-spaces.limits-of-cauchy-approximations-in-premetric-spaces
+open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.short-functions-metric-spaces
 ```