Zulip Chat Archive

Stream: maths

Topic: Uniqueness of the reals


view this post on Zulip Kevin Buzzard (Oct 16 2019 at 08:28):

Does mathlib have the theorem that the reals is "the unique complete archimedean field" (this can be made precise)?

view this post on Zulip Kevin Buzzard (Oct 16 2019 at 08:28):

I'm giving a lecture about this in 90 minutes ;-)

view this post on Zulip Mario Carneiro (Oct 16 2019 at 08:28):

the uniqueness is not proved

view this post on Zulip Mario Carneiro (Oct 16 2019 at 08:29):

we would need real.cast which hasn't been defined yet

view this post on Zulip Mario Carneiro (Oct 16 2019 at 08:30):

If you have any conditionally complete ordered division ring A I think you can define a function real.cast : real -> A by extending rat.cast continuously. I'm not sure if that's the best constraint

view this post on Zulip Mario Carneiro (Oct 16 2019 at 08:32):

If you had some kind of sequential completeness assumption, the function could probably be computable too

view this post on Zulip Mario Carneiro (Oct 16 2019 at 08:38):

I think you can use dense_embedding to extend rat.cast if you know complete_space A

view this post on Zulip Kevin Buzzard (Oct 16 2019 at 08:55):

I am not necessarily going to use much Lean in this lecture, but basically the more we have the merrier.

view this post on Zulip Kevin Buzzard (Oct 16 2019 at 08:55):

If you have any conditionally complete ordered division ring A I think you can define a function real.cast : real -> A by extending rat.cast continuously. I'm not sure if that's the best constraint

This sounds like a job for @Patrick Massot but he's probably popping the champagne after getting our paper finished ;-)


Last updated: May 12 2021 at 07:17 UTC