Documentation

Mathlib.Data.Real.Cardinality

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 #

Main statements #

Notation #

Tags #

continuum, cardinality, reals, cardinality of the reals

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
Instances For
    @[simp]
    theorem Cardinal.cantorFunctionAux_true {c : } {f : Bool} {n : } (h : f n = true) :
    @[simp]
    theorem Cardinal.cantorFunctionAux_false {c : } {f : Bool} {n : } (h : f n = false) :
    theorem Cardinal.cantorFunctionAux_nonneg {c : } {f : Bool} {n : } (h : 0 c) :
    theorem Cardinal.cantorFunctionAux_eq {c : } {f : Bool} {g : Bool} {n : } (h : f n = g n) :
    theorem Cardinal.cantorFunctionAux_zero {c : } (f : Bool) :
    Cardinal.cantorFunctionAux c f 0 = bif f 0 then 1 else 0
    theorem Cardinal.cantorFunctionAux_succ {c : } (f : Bool) :
    (fun (n : ) => Cardinal.cantorFunctionAux c f (n + 1)) = fun (n : ) => c * Cardinal.cantorFunctionAux c (fun (n : ) => f (n + 1)) n
    theorem Cardinal.summable_cantor_function {c : } (f : Bool) (h1 : 0 c) (h2 : c < 1) :
    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
    Instances For
      theorem Cardinal.cantorFunction_le {c : } {f : Bool} {g : Bool} (h1 : 0 c) (h2 : c < 1) (h3 : ∀ (n : ), f n = trueg n = true) :
      theorem Cardinal.cantorFunction_succ {c : } (f : Bool) (h1 : 0 c) (h2 : c < 1) :
      Cardinal.cantorFunction c f = (bif f 0 then 1 else 0) + c * Cardinal.cantorFunction c fun (n : ) => f (n + 1)
      theorem Cardinal.increasing_cantorFunction {c : } (h1 : 0 < c) (h2 : c < 1 / 2) {n : } {f : Bool} {g : Bool} (hn : k < n, f k = g k) (fn : f n = false) (gn : g n = true) :

      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.

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

      The cardinality of the reals, as a type.

      The cardinality of the reals, as a set.

      theorem Cardinal.not_countable_real :
      ¬Set.univ.Countable

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