Commit 2022-09-26 19:49 9f972c7e

feat(topology/uniform_space/completion): add uniform_completion.complete_equiv_self (#16612)

• Change abstract_completion.compare_equiv to uniform bijection.
• Define the abstract_completion α given by α when it is complete.
• Use it to prove that there is a uniform bijection between a complete space and its uniform_completion.
• Upgrade the bijection between Bourbaki reals and Cauchy reals to a uniform bijection.
• Add a new function function.dense_range_id (needed in one of the proofs)