# The cardinality of the reals #

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 #

- `Cardinal.cantorFunction` is the function that sends `f` in `{0, 1} ^ ℕ` to `ℝ` by `f ↦ Σ' n, f n * (1 / 3) ^ n`

## Main statements #

- `Cardinal.mk_real : #ℝ = 𝔠`: 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.

## Notation #

- `𝔠` : notation for `Cardinal.continuum` in scope `Cardinal`, defined in `SetTheory.Continuum`.

## Tags #

continuum, cardinality, reals, cardinality of the reals

source
def Cardinal.cantorFunctionAux (c : ℝ) (f : ℕ → Bool) (n : ℕ) :
ℝ

The body of the sum in `cantorFunction`. `cantorFunctionAux c f n = c ^ n` if `f n = true`; `cantorFunctionAux c f n = 0` if `f n = false`.

Equations

- Cardinal.cantorFunctionAux c f n = bif f n then c ^ n else 0

Instances For

source
@[simp]
theorem Cardinal.cantorFunctionAux_true {c : ℝ} {f : ℕ → Bool} {n : ℕ} (h : f n = true) :
cantorFunctionAux c f n = c ^ n
source
@[simp]
theorem Cardinal.cantorFunctionAux_false {c : ℝ} {f : ℕ → Bool} {n : ℕ} (h : f n = false) :
cantorFunctionAux c f n = 0
source
theorem Cardinal.cantorFunctionAux_nonneg {c : ℝ} {f : ℕ → Bool} {n : ℕ} (h : 0 ≤ c) :
0 ≤ cantorFunctionAux c f n
source
theorem Cardinal.cantorFunctionAux_eq {c : ℝ} {f g : ℕ → Bool} {n : ℕ} (h : f n = g n) :
cantorFunctionAux c f n = cantorFunctionAux c g n
source
theorem Cardinal.cantorFunctionAux_zero {c : ℝ} (f : ℕ → Bool) :
cantorFunctionAux c f 0 = bif f 0 then 1 else 0
source
theorem Cardinal.cantorFunctionAux_succ {c : ℝ} (f : ℕ → Bool) :
(fun (n : ℕ) => cantorFunctionAux c f (n + 1)) = fun (n : ℕ) => c * cantorFunctionAux c (fun (n : ℕ) => f (n + 1)) n
source
theorem Cardinal.summable_cantor_function {c : ℝ} (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) :
Summable (cantorFunctionAux c f)
source
def Cardinal.cantorFunction (c : ℝ) (f : ℕ → Bool) :
ℝ

`cantorFunction c (f : ℕ → Bool)` is `Σ n, f n * c ^ n`, where `true` is interpreted as `1` and `false` is interpreted as `0`. It is implemented using `cantorFunctionAux`.

Equations

- Cardinal.cantorFunction c f = ∑' (n : ℕ), Cardinal.cantorFunctionAux c f n

Instances For

source
theorem Cardinal.cantorFunction_le {c : ℝ} {f g : ℕ → Bool} (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ (n : ℕ), f n = true → g n = true) :
cantorFunction c f ≤ cantorFunction c g
source
theorem Cardinal.cantorFunction_succ {c : ℝ} (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) :
cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun (n : ℕ) => f (n + 1)
source
theorem Cardinal.increasing_cantorFunction {c : ℝ} (h1 : 0 < c) (h2 : c < 1 / 2) {n : ℕ} {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true) :
cantorFunction c f < cantorFunction c g

`cantorFunction 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.cantorFunction_injective {c : ℝ} (h1 : 0 < c) (h2 : c < 1 / 2) :
Function.Injective (cantorFunction c)

`cantorFunction c` is injective if `0 < c < 1/2`.

source
theorem Cardinal.mk_real :
mk ℝ = continuum

The cardinality of the reals, as a type.

source
theorem Cardinal.mk_univ_real :
mk ↑Set.univ = continuum

The cardinality of the reals, as a set.

source
instance Cardinal.instUncountableReal :
Uncountable ℝ

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

source
theorem Cardinal.not_countable_real :
¬Set.univ.Countable
source
theorem Cardinal.mk_Ioi_real (a : ℝ) :
mk ↑(Set.Ioi a) = continuum

The cardinality of the interval (a, ∞).

source
theorem Cardinal.mk_Ici_real (a : ℝ) :
mk ↑(Set.Ici a) = continuum

The cardinality of the interval [a, ∞).

source
theorem Cardinal.mk_Iio_real (a : ℝ) :
mk ↑(Set.Iio a) = continuum

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

source
theorem Cardinal.mk_Iic_real (a : ℝ) :
mk ↑(Set.Iic a) = continuum

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

source
theorem Cardinal.mk_Ioo_real {a b : ℝ} (h : a < b) :
mk ↑(Set.Ioo a b) = continuum

The cardinality of the interval (a, b).

source
theorem Cardinal.mk_Ico_real {a b : ℝ} (h : a < b) :
mk ↑(Set.Ico a b) = continuum

The cardinality of the interval [a, b).

source
theorem Cardinal.mk_Icc_real {a b : ℝ} (h : a < b) :
mk ↑(Set.Icc a b) = continuum

The cardinality of the interval [a, b].

source
theorem Cardinal.mk_Ioc_real {a b : ℝ} (h : a < b) :
mk ↑(Set.Ioc a b) = continuum

The cardinality of the interval (a, b].

source
@[simp]
theorem Cardinal.Real.Ioo_countable_iff {x y : ℝ} :
(Set.Ioo x y).Countable ↔ y ≤ x
source
@[simp]
theorem Cardinal.Real.Ico_countable_iff {x y : ℝ} :
(Set.Ico x y).Countable ↔ y ≤ x
source
@[simp]
theorem Cardinal.Real.Ioc_countable_iff {x y : ℝ} :
(Set.Ioc x y).Countable ↔ y ≤ x
source
@[simp]
theorem Cardinal.Real.Icc_countable_iff {x y : ℝ} :
(Set.Icc x y).Countable ↔ y ≤ x