The Cardinality of the Continuum

Manuel Eberl
Archive of Formal Proofs 2023.

pdf AFP entry

Abstract

This entry presents a short derivation of the cardinality of the real numbers, namely that it is the same as the cardinality of the power set of the naturals. This is done by giving an injection in both directions: in the one direction via Dedekind cuts, in the other direction via ternary fractions.

BibTex

@article{Cardinality_Continuum-AFP,
author = {Manuel Eberl},
title = {The Cardinality of the Continuum},
journal = {Archive of Formal Proofs},
month = {November},
year = {2023},
note = {\url{https://isa-afp.org/entries/Cardinality_Continuum.html},
Formal proof development},
ISSN = {2150-914x},
}