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},
}