Limits of sequences in metric spaces

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
 ```