mathlib documentation

data.real.cardinality

The cardinality of the reals

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

We shows that #ℝ ≤ 2^ω by noting that every real number is determined by a Cauchy-sequence of the form ℕ → ℚ, which has cardinality 2^ω. To show that #ℝ ≥ 2^ω 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

Main statements

Tags

continuum, cardinality, reals, cardinality of the reals

def cardinal.cantor_function_aux  :
(bool)

The body of the sum in cantor_function. cantor_function_aux c f n = c ^ n if f n = tt; cantor_function_aux c f n = 0 if f n = ff.

Equations
@[simp]
theorem cardinal.cantor_function_aux_tt {c : } {f : bool} {n : } :
f n = ttcardinal.cantor_function_aux c f n = c ^ n

@[simp]
theorem cardinal.cantor_function_aux_ff {c : } {f : bool} {n : } :

theorem cardinal.cantor_function_aux_nonneg {c : } {f : bool} {n : } :

theorem cardinal.cantor_function_aux_succ {c : } (f : bool) :
(λ (n : ), cardinal.cantor_function_aux c f (n + 1)) = λ (n : ), c * cardinal.cantor_function_aux c (λ (n : ), f (n + 1)) n

def cardinal.cantor_function  :
(bool)

cantor_function c (f : ℕ → bool) is Σ n, f n * c ^ n, where tt is interpreted as 1 and ff is interpreted as 0. It is implemented using cantor_function_aux.

Equations
theorem cardinal.cantor_function_le {c : } {f g : bool} :
0 cc < 1(∀ (n : ), (f n)(g n))cardinal.cantor_function c f cardinal.cantor_function c g

theorem cardinal.cantor_function_succ {c : } (f : bool) :
0 cc < 1cardinal.cantor_function c f = cond (f 0) 1 0 + c * cardinal.cantor_function c (λ (n : ), f (n + 1))

theorem cardinal.increasing_cantor_function {c : } (h1 : 0 < c) (h2 : c < 1 / 2) {n : } {f g : bool} :
(∀ (k : ), k < nf k = g k)f n = ffg n = ttcardinal.cantor_function c f < cardinal.cantor_function c g

cantor_function 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.

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

The cardinality of the reals, as a type.

The cardinality of the reals, as a set.

The reals are not countable.

The cardinality of the interval (a, ∞).

The cardinality of the interval [a, ∞).

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

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

theorem cardinal.mk_Ioo_real {a b : } :
a < b# (set.Ioo a b) = 2 ^ cardinal.omega

The cardinality of the interval (a, b).

theorem cardinal.mk_Ico_real {a b : } :
a < b# (set.Ico a b) = 2 ^ cardinal.omega

The cardinality of the interval [a, b).

theorem cardinal.mk_Icc_real {a b : } :
a < b# (set.Icc a b) = 2 ^ cardinal.omega

The cardinality of the interval [a, b].

theorem cardinal.mk_Ioc_real {a b : } :
a < b# (set.Ioc a b) = 2 ^ cardinal.omega

The cardinality of the interval (a, b].