generalize continuous_comp_cvg

[t6s]

Motivation for this change

This PR is a strict generalization of lemma continuous_comp_cvg that has been in pseudometric_structure.v pseudometric_normed_Zmodule.v.

NB: the name continuous_comp_cvg does not look very good considering similar lemmas continuous_cvg and cvg_comp.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Thanks for the generalization! Let's add id_continuous because incidentally we also needed the lemma in another piece of work (and I also remember this was due some performance problem but maybe not a Search).