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_functionis the function that sendsfin{0, 1} ^ ℕtoℝbyf ↦ Σ' 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_realforx,y ∈ {i,o,c}state that intervals on the reals have cardinality continuum.
Tags
continuum, cardinality, reals, cardinality of the reals
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
- cardinal.cantor_function c f = ∑' (n : ℕ), cardinal.cantor_function_aux c f n
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 cardinality of the interval (a, ∞).
The cardinality of the interval [a, ∞).
The cardinality of the interval (-∞, a).
The cardinality of the interval (-∞, a].
The cardinality of the interval (a, b).
The cardinality of the interval [a, b).
The cardinality of the interval [a, b].
The cardinality of the interval (a, b].