Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-26 19:49 9f972c7e

View on Github →

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)

Estimated changes