Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Constructing the Reals as Dede...

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: Jan 04 2025 at 20:18 UTC