Stream: Coq users

Topic: ✔ How to prove that R is complete space?

Lessness (Nov 22 2021 at 21:03):

In other words, how to prove that every Cauchy sequence is convergent.
Is there some good proof of it in Coq? In standard library or somewhere else...

Because I'm having problems translating the proof of book to Coq. :(

Lessness (Nov 23 2021 at 14:42):

False alert, I managed to do it. :)

Notification Bot (Nov 23 2021 at 14:42):

Lessness has marked this topic as resolved.

Karl Palmskog (Nov 23 2021 at 14:43):

given that the Stdlib now has Cauchy sequences, I think this fact must be in Stdlib as well...

Last updated: Oct 13 2024 at 01:02 UTC