| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Constructing the Reals as Dedekind Cuts of Rationals
| Title: | Constructing the Reals as Dedekind Cuts of Rationals |
| Authors: | Jacques D. Fleuriot and Lawrence C. Paulson |
| Submission date: | 2022-03-24 |
| Abstract: | 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. |
| BibTeX: |
@article{Dedekind_Real-AFP,
author = {Jacques D. Fleuriot and Lawrence C. Paulson},
title = {Constructing the Reals as Dedekind Cuts of Rationals},
journal = {Archive of Formal Proofs},
month = mar,
year = 2022,
note = {\url{https://isa-afp.org/entries/Dedekind_Real.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |