Stream: Coq users

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


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

view this post on Zulip Lessness (Nov 23 2021 at 14:42):

False alert, I managed to do it. :)

view this post on Zulip Notification Bot (Nov 23 2021 at 14:42):

Lessness has marked this topic as resolved.

view this post on Zulip 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: Feb 04 2023 at 22:29 UTC