Limits of sequences in metric spaces

[malarbol]

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.

[malarbol]

It feels like the for module

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

should be renamed

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

(remove some -in and add some -of).
Do you agree?

[fredrik-bakke]

By the way (this is outside the scope of this PR), I might also suggest using the term "indiscernible" for what you currently call "indistinguishable". This fits with the principle of Identity of indiscernibles. Personally, I actually first learned about this principle in the context of metric spaces! This also meshes with the terminology of the book The Univalence Principle, which coincidentally I was following for #1419.

[fredrik-bakke]

It feels like the for module

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

should be renamed

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

(remove some -in and add some -of). Do you agree?

Yes, this seems reasonable

[fredrik-bakke]

Thank you for this excellent addition!

[malarbol]

If the content is ok, I think maybe we could add some ## See also between some modules
(e.g. limits-of-sequences --> convergent-sequences --> metric-space-of-convergent-sequences).
Also, I guess we could add some references (e.g. https://en.wikipedia.org/wiki/Limit_of_a_sequence) and Wikidata entries.

[fredrik-bakke]

Oh, sure, please do. Let me know when you are done with those final additions

[malarbol]

By the way (this is outside the scope of this PR), I might also suggest using the term "indiscernible" for what you currently call "indistinguishable". This fits with the principle of Identity of indiscernibles. Personally, I actually first learned about this principle in the context of metric spaces! This also meshes with the terminology of the book The Univalence Principle, which coincidentally I was following for #1419.

One problem is that, even if it's defined for premetric spaces in general, you need at least a pseudometric structure to make it an equivalence relation. so "indiscernible" doesn't seem right for premetric spaces. I'll open an Issue to discuss renaming/refactoring the metric-spaces module as we discussed already and we can talk about it.
I'm starting to think the hierarchy premetric -> pseudometric -> metric is a bit too much and we could do with only premetric (what we call pseudometric now) and metric, a premetric space where "indiscernible" elements are equal.

[malarbol]

Oh, sure, please do. Let me know when you are done with those final additions

That's done.

[malarbol]

Thank you for this excellent addition!

Thanks. I still haven't proved (r < 1)ⁿ → 0, I took the long way I guess, but I hope this proves useful in the future.