Stream: Is there code for X?
Topic: reals are unique
Kevin Buzzard (Aug 06 2020 at 16:08):
Did we ever get one or both of "two complete totally ordered archimedean fields are equiv" or "a complete totally ordered archimedean field is equiv to \R"?
Bryan Gin-ge Chen (Aug 06 2020 at 16:35):
I think this is in #3292 by @Alex J. Best.
Alex J. Best (Aug 06 2020 at 16:36):
Johan left me some great comments, but I haven't had much lean time to implement them yet
Alex J. Best (Aug 06 2020 at 16:55):
If anyone wants to make any changes feel free to do so by the way, I just haven't had the chance to myself and really don't have a strong opinion RE: naming and what files things should go in.
Last updated: May 16 2021 at 05:21 UTC