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

source
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
source
@[simp]
theorem cardinal.cantor_function_aux_tt {c : ℝ} {f : ℕ → bool} {n : ℕ} (h : f n = bool.tt) :
cardinal.cantor_function_aux c f n = c ^ n
source
@[simp]
theorem cardinal.cantor_function_aux_ff {c : ℝ} {f : ℕ → bool} {n : ℕ} (h : f n = bool.ff) :
cardinal.cantor_function_aux c f n = 0
source
theorem cardinal.cantor_function_aux_nonneg {c : ℝ} {f : ℕ → bool} {n : ℕ} (h : 0 ≤ c) :
0 ≤ cardinal.cantor_function_aux c f n
source
theorem cardinal.cantor_function_aux_eq {c : ℝ} {f g : ℕ → bool} {n : ℕ} (h : f n = g n) :
cardinal.cantor_function_aux c f n = cardinal.cantor_function_aux c g n
source
theorem cardinal.cantor_function_aux_zero {c : ℝ} (f : ℕ → bool) :
cardinal.cantor_function_aux c f 0 = cond (f 0) 1 0
source
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
source
theorem cardinal.summable_cantor_function {c : ℝ} (f : ℕ → bool) (h1 : 0 ≤ c) (h2 : c < 1) :
summable (cardinal.cantor_function_aux c f)
source
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
source
theorem cardinal.cantor_function_le {c : ℝ} {f g : ℕ → bool} (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ (n : ℕ), ↥(f n) → ↥(g n)) :
cardinal.cantor_function c f ≤ cardinal.cantor_function c g
source
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))
source
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) :
cardinal.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.

source
theorem cardinal.cantor_function_injective {c : ℝ} (h1 : 0 < c) (h2 : c < 1 / 2) :
function.injective (cardinal.cantor_function c)

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

source
theorem cardinal.mk_real  :
cardinal.mk ℝ = cardinal.continuum

The cardinality of the reals, as a type.

source
theorem cardinal.mk_univ_real  :
cardinal.mk ↥set.univ = cardinal.continuum

The cardinality of the reals, as a set.

source
theorem cardinal.not_countable_real  :
¬set.univ.countable

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

source
theorem cardinal.mk_Ioi_real (a : ℝ) :
cardinal.mk ↥(set.Ioi a) = cardinal.continuum

The cardinality of the interval (a, ∞).

source
theorem cardinal.mk_Ici_real (a : ℝ) :
cardinal.mk ↥(set.Ici a) = cardinal.continuum

The cardinality of the interval [a, ∞).

source
theorem cardinal.mk_Iio_real (a : ℝ) :
cardinal.mk ↥(set.Iio a) = cardinal.continuum

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

source
theorem cardinal.mk_Iic_real (a : ℝ) :
cardinal.mk ↥(set.Iic a) = cardinal.continuum

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

source
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).

source
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).

source
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].

source
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].