Topic: metric space competion
Sebastien Gouezel (Feb 19 2019 at 17:09):
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 (Feb 19 2019 at 20:16):
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 (Feb 20 2019 at 22:20):
Now it is there, in #PR743
Patrick Massot (Feb 20 2019 at 22:25):
Patrick Massot (Feb 20 2019 at 22:28):
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 (Feb 21 2019 at 08:24):
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!
Last updated: May 10 2021 at 07:15 UTC