mathlib

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

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)