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
@@ -69,8 +70,12 @@ 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-sequences-metric-spaces public
+open import metric-spaces.limits-sequences-premetric-spaces public
+open import metric-spaces.limits-sequences-pseudometric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-in-a-metric-space public
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-in-a-metric-space 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
@@ -86,6 +91,9 @@ open import metric-spaces.pseudometric-spaces public
 open import metric-spaces.pseudometric-structures public
 open import metric-spaces.reflexive-premetric-structures 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