# Documentation

Mathlib.Data.Real.Cardinality

# The cardinality of the reals #

This file shows that the real numbers have cardinality continuum, i.e. #ℝ = 𝔠.

We show that #ℝ ≤ 𝔠 by noting that every real number is determined by a Cauchy-sequence of the form ℕ → ℚ, which has cardinality 𝔠. To show that #ℝ ≥ 𝔠 we define an injection from {0, 1} ^ ℕ to ℝ with f ↦ Σ n, f n * (1 / 3) ^ n.

We conclude that all intervals with distinct endpoints have cardinality continuum.

## Main definitions #

• Cardinal.cantorFunction is the function that sends f in {0, 1} ^ ℕ to ℝ by f ↦ Σ' n, f n * (1 / 3) ^ n

## Main statements #

• Cardinal.mk_real : #ℝ = 𝔠: the reals have cardinality continuum.
• Cardinal.not_countable_real: the universal set of real numbers is not countable. We can use this same proof to show that all the other sets in this file are not countable.
• 8 lemmas of the form mk_Ixy_real for x,y ∈ {i,o,c} state that intervals on the reals have cardinality continuum.

## Notation #

• 𝔠 : notation for Cardinal.Continuum in locale Cardinal, defined in SetTheory.Continuum.

## Tags #

continuum, cardinality, reals, cardinality of the reals

def Cardinal.cantorFunctionAux (c : ) (f : ) (n : ) :

The body of the sum in cantorFunction. cantorFunctionAux c f n = c ^ n if f n = true; cantorFunctionAux c f n = 0 if f n = false.

Instances For
@[simp]
theorem Cardinal.cantorFunctionAux_true {c : } {f : } {n : } (h : f n = true) :
= c ^ n
@[simp]
theorem Cardinal.cantorFunctionAux_false {c : } {f : } {n : } (h : f n = false) :
= 0
theorem Cardinal.cantorFunctionAux_nonneg {c : } {f : } {n : } (h : 0 c) :
0
theorem Cardinal.cantorFunctionAux_eq {c : } {f : } {g : } {n : } (h : f n = g n) :
theorem Cardinal.cantorFunctionAux_zero {c : } (f : ) :
= bif f 0 then 1 else 0
theorem Cardinal.cantorFunctionAux_succ {c : } (f : ) :
(fun n => Cardinal.cantorFunctionAux c f (n + 1)) = fun n => c * Cardinal.cantorFunctionAux c (fun n => f (n + 1)) n
theorem Cardinal.summable_cantor_function {c : } (f : ) (h1 : 0 c) (h2 : c < 1) :
def Cardinal.cantorFunction (c : ) (f : ) :

cantorFunction c (f : ℕ → Bool) is Σ n, f n * c ^ n, where true is interpreted as 1 and false is interpreted as 0. It is implemented using cantorFunctionAux.

Instances For
theorem Cardinal.cantorFunction_le {c : } {f : } {g : } (h1 : 0 c) (h2 : c < 1) (h3 : ∀ (n : ), f n = trueg n = true) :
theorem Cardinal.cantorFunction_succ {c : } (f : ) (h1 : 0 c) (h2 : c < 1) :
= (bif f 0 then 1 else 0) + c * Cardinal.cantorFunction c fun n => f (n + 1)
theorem Cardinal.increasing_cantorFunction {c : } (h1 : 0 < c) (h2 : c < 1 / 2) {n : } {f : } {g : } (hn : ∀ (k : ), k < nf k = g k) (fn : f n = false) (gn : g n = true) :

cantorFunction c is strictly increasing with if 0 < c < 1/2, if we endow ℕ → Bool with a lexicographic order. The lexicographic order doesn't exist for these infinitary products, so we explicitly write out what it means.

theorem Cardinal.cantorFunction_injective {c : } (h1 : 0 < c) (h2 : c < 1 / 2) :

cantorFunction c is injective if 0 < c < 1/2.

The cardinality of the reals, as a type.

The cardinality of the reals, as a set.

Non-Denumerability of the Continuum: The reals are not countable.

theorem Cardinal.mk_Ioi_real (a : ) :

The cardinality of the interval (a, ∞).

theorem Cardinal.mk_Ici_real (a : ) :

The cardinality of the interval [a, ∞).

theorem Cardinal.mk_Iio_real (a : ) :

The cardinality of the interval (-∞, a).

theorem Cardinal.mk_Iic_real (a : ) :

The cardinality of the interval (-∞, a].

theorem Cardinal.mk_Ioo_real {a : } {b : } (h : a < b) :

The cardinality of the interval (a, b).

theorem Cardinal.mk_Ico_real {a : } {b : } (h : a < b) :

The cardinality of the interval [a, b).

theorem Cardinal.mk_Icc_real {a : } {b : } (h : a < b) :

The cardinality of the interval [a, b].

theorem Cardinal.mk_Ioc_real {a : } {b : } (h : a < b) :

The cardinality of the interval (a, b].