[Merged by Bors] - feat(Topology/UniformSpace/AbstractCompletion):add comparison lemma

[faenuccio]

Add a lemma showing that composing the comparison maps with a continuous function to a T3 space satisfying some conditions yield the same function.

Co-authored with : María Inés de Frutos Fernández @mariainesdff

[github-actions]

PR summary bcf0b5b6d9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ compare_comp_eq_compare

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[faenuccio]

I have addressed @urkud 's comments, but I had a private DM with @PatrickMassot who thinks the result is too specialized. IMHO it is OK and it is at the same time useful to have this comparison result, stated under quite general assumptions, but not too general as to be practically unapplicable (I will indeed need it in a later PR proving an equivalence between Laurent series and the X-adic completion of rational functions). I wonder how to advance now.

[PatrickMassot]

bors d+

[mathlib-bors]

✌️ faenuccio can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[faenuccio]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style