Zulip Chat Archive

Stream: maths

Topic: metric space competion


view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Feb 20 2019 at 22:20):

Now it is there, in #PR743

view this post on Zulip Patrick Massot (Feb 20 2019 at 22:25):

Nice!

view this post on Zulip 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

view this post on Zulip 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