Email Gateway (Mar 29 2022 at 06:31): Email Gateway (Mar 29 2022 at 06:31):From: Tobias Nipkow <nipkow@in.tum.de>
Constructing the Reals as Dedekind Cuts of Rationals
Jacques D. Fleuriot and Lawrence C. Paulson
The type of real numbers is constructed from the positive rationals using the
method of Dedekind cuts. This development, briefly described in papers by the
authors, follows the textbook presentation by Gleason. It's notable that the
first formalisation of a significant piece of mathematics, by Jutting in 1977,
involved a similar construction.
https://www.isa-afp.org/entries/Dedekind_Real.html
This formalization was moved to the AFP from the distribution (HOL/ex/)
Enjoy!
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC