### Abstract

This entry presents a short derivation of the cardinality of $\mathbb{R}$, namely that $|\mathbb{R}| = |2^{\mathbb{N}}| = 2^{\aleph_0}$. This is done by showing the injection $\mathbb{R}\to 2^{\mathbb{Q}},\ x \mapsto (-\infty, x)\cap\mathbb{Q}$ (i.e. Dedekind cuts) for one direction and the injection $2^\mathbb{N}\to\mathbb{Q},\ X \mapsto \sum_{n\in X} 3^{-n}$, i.e. ternary fractions, for the other direction.

### License

BSD License

### Topics

- Logic/Set theory

### Session Cardinality_Continuum

- Cardinality_Continuum_Library
- Cardinality_Continuum
- Cardinality_Euclidean_Space

## Cite

×

Cardinality_Continuum-AFP

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

Download

## Download

× Download latest