mathlib3 documentation

data.real.cardinality

The cardinality of the reals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main statements #

Notation #

Tags #

continuum, cardinality, reals, cardinality of the reals

def cardinal.cantor_function_aux (c : ) (f : bool) (n : ) :

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 : } (h : f n = bool.tt) :
@[simp]
theorem cardinal.cantor_function_aux_ff {c : } {f : bool} {n : } (h : f n = bool.ff) :
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
theorem cardinal.summable_cantor_function {c : } (f : bool) (h1 : 0 c) (h2 : c < 1) :
noncomputable def cardinal.cantor_function (c : ) (f : 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} (h1 : 0 c) (h2 : c < 1) (h3 : (n : ), (f n) (g n)) :
theorem cardinal.cantor_function_succ {c : } (f : bool) (h1 : 0 c) (h2 : c < 1) :
cardinal.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} (hn : (k : ), k < n f k = g k) (fn : f n = bool.ff) (gn : g n = bool.tt) :

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.

Non-Denumerability of the Continuum: 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 : } (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].