metric space competion

Stream: maths

[Sebastien Gouezel]

I could not locate in mathlib the fact that the (uniform space) completion of a metric space is also a metric space. Can someone confirm that it is not there (yet)?

[Patrick Massot]

It's clearly not there. The whole completion stuff is waiting for available time from Johannes or Reid. I don't want to PR more stuff until the topology reorganization happens.

[Sebastien Gouezel]

Now it is there, in #PR743

[Patrick Massot]

Nice!

[Patrick Massot]

I hope it will nicely survive any later refactor (I do plan to to switch to Bourbaki's construction of the completion, Johannes' method needs too many workarounds). My hope is that I'll have time for Lean during my vacations I have an ankle strain that will prevent me from skiing or hiking. Then I hope to restart on splitting topology files, hoping to open a PR and get it merged fast enough to avoid wasting too much energy (or redo it a third time). Then I hope to improve the uniform space theory, and finally finish completion properly

[Sebastien Gouezel]

I only use the interface (completion.extension that extends a uniformly continuous function to a uniformly continuous function on the completion, and induction_on saying that a closed property holds on the completion iff it holds on the base). So, hopefully, this should survive any refactor without requiring any modification. By the way, this shows that the interface is pretty good!