# mathlibdocumentation

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 #

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

## Main statements #

• cardinal.mk_real : #ℝ = 2 ^ omega: 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.

## 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 = tt) :
= c ^ n
@[simp]
theorem cardinal.cantor_function_aux_ff {c : } {f : bool} {n : } (h : f n = ff) :
theorem cardinal.cantor_function_aux_nonneg {c : } {f : bool} {n : } (h : 0 c) :
theorem cardinal.cantor_function_aux_eq {c : } {f g : bool} {n : } (h : f n = g n) :
theorem cardinal.cantor_function_aux_succ {c : } (f : bool) :
(λ (n : ), (n + 1)) = λ (n : ), c * (λ (n : ), f (n + 1)) n
theorem cardinal.summable_cantor_function {c : } (f : bool) (h1 : 0 c) (h2 : c < 1) :
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) :
= cond (f 0) 1 0 + 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 < nf k = g k) (fn : f n = ff) (gn : g n = 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.

theorem cardinal.cantor_function_injective {c : } (h1 : 0 < c) (h2 : c < 1 / 2) :

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

theorem cardinal.mk_real  :

The cardinality of the reals, as a type.

theorem cardinal.mk_univ_real  :

The cardinality of the reals, as a set.

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) :
# (set.Ioo a b) =

The cardinality of the interval (a, b).

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

The cardinality of the interval [a, b).

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

The cardinality of the interval [a, b].

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

The cardinality of the interval (a, b].