Uniqueness of the reals

Stream: maths

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

the uniqueness is not proved

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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 ;-)