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 : ℕ → Bool) (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.

Equations

• Cardinal.cantorFunctionAux c f n = bif f n then c ^ n else 0

@[simp]

theorem Cardinal.cantorFunctionAux_true {c : ℝ} {f : ℕ → Bool} {n : ℕ} (h : f n = true) : Cardinal.cantorFunctionAux c f n = c ^ n

@[simp]

theorem Cardinal.cantorFunctionAux_false {c : ℝ} {f : ℕ → Bool} {n : ℕ} (h : f n = false) : Cardinal.cantorFunctionAux c f n = 0

theorem Cardinal.cantorFunctionAux_nonneg {c : ℝ} {f : ℕ → Bool} {n : ℕ} (h : 0 ≤ c) : 0 ≤ Cardinal.cantorFunctionAux c f n

theorem Cardinal.cantorFunctionAux_eq {c : ℝ} {f : ℕ → Bool} {g : ℕ → Bool} {n : ℕ} (h : f n = g n) : Cardinal.cantorFunctionAux c f n = Cardinal.cantorFunctionAux c g n

theorem Cardinal.cantorFunctionAux_zero {c : ℝ} (f : ℕ → Bool) : Cardinal.cantorFunctionAux c f 0 = bif f 0 then 1 else 0

theorem Cardinal.cantorFunctionAux_succ {c : ℝ} (f : ℕ → Bool) : (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 : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) : Summable (Cardinal.cantorFunctionAux c f)

def Cardinal.cantorFunction (c : ℝ) (f : ℕ → Bool) : ℝ

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.

Equations

• Cardinal.cantorFunction c f = ∑' (n : ℕ), Cardinal.cantorFunctionAux c f n

theorem Cardinal.cantorFunction_le {c : ℝ} {f : ℕ → Bool} {g : ℕ → Bool} (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ (n : ℕ), f n = true → g n = true) : Cardinal.cantorFunction c f ≤ Cardinal.cantorFunction c g

theorem Cardinal.cantorFunction_succ {c : ℝ} (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) : Cardinal.cantorFunction c f = (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 : ℕ → Bool} {g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true) : Cardinal.cantorFunction c f < Cardinal.cantorFunction c g

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) : Function.Injective (Cardinal.cantorFunction c)

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

theorem Cardinal.mk_real : Cardinal.mk ℝ = Cardinal.continuum

The cardinality of the reals, as a type.

theorem Cardinal.mk_univ_real : Cardinal.mk ↑Set.univ = Cardinal.continuum

The cardinality of the reals, as a set.

theorem Cardinal.not_countable_real : ¬Set.univ.Countable

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

theorem Cardinal.mk_Ioi_real (a : ℝ) : Cardinal.mk ↑(Set.Ioi a) = Cardinal.continuum

The cardinality of the interval (a, ∞).

theorem Cardinal.mk_Ici_real (a : ℝ) : Cardinal.mk ↑(Set.Ici a) = Cardinal.continuum

The cardinality of the interval [a, ∞).

theorem Cardinal.mk_Iio_real (a : ℝ) : Cardinal.mk ↑(Set.Iio a) = Cardinal.continuum

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

theorem Cardinal.mk_Iic_real (a : ℝ) : Cardinal.mk ↑(Set.Iic a) = Cardinal.continuum

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

theorem Cardinal.mk_Ioo_real {a : ℝ} {b : ℝ} (h : a < b) : Cardinal.mk ↑(Set.Ioo a b) = Cardinal.continuum

The cardinality of the interval (a, b).

theorem Cardinal.mk_Ico_real {a : ℝ} {b : ℝ} (h : a < b) : Cardinal.mk ↑(Set.Ico a b) = Cardinal.continuum

The cardinality of the interval [a, b).

theorem Cardinal.mk_Icc_real {a : ℝ} {b : ℝ} (h : a < b) : Cardinal.mk ↑(Set.Icc a b) = Cardinal.continuum

The cardinality of the interval [a, b].

theorem Cardinal.mk_Ioc_real {a : ℝ} {b : ℝ} (h : a < b) : Cardinal.mk ↑(Set.Ioc a b) = Cardinal.continuum

The cardinality of the interval (a, b].