mathlib documentation

set_theory.continuum

Cardinality of continuum #

In this file we define cardinal.continuum (notation: 𝔠, localized in cardinal) to be 2 ^ ω. We also prove some simp lemmas about cardinal arithmetic involving 𝔠.

Notation #

source
def cardinal.continuum  :
cardinal

Cardinality of continuum.

Equations
source
@[simp]
theorem cardinal.two_power_omega  :
2 ^ ω = 𝔠
source
@[simp]
theorem cardinal.lift_continuum  :
𝔠.lift = 𝔠

Inequalities #

source
theorem cardinal.omega_lt_continuum  :
ω < 𝔠
source
theorem cardinal.omega_le_continuum  :
ω ≤ 𝔠
source
theorem cardinal.nat_lt_continuum (n : ℕ) :
↑n < 𝔠
source
theorem cardinal.mk_set_nat  :
# (set ℕ) = 𝔠
source
theorem cardinal.continuum_pos  :
0 < 𝔠
source
theorem cardinal.continuum_ne_zero  :
𝔠 ≠ 0

Addition #

source
@[simp]
theorem cardinal.omega_add_continuum  :
ω + 𝔠 = 𝔠
source
@[simp]
theorem cardinal.continuum_add_omega  :
𝔠 + ω = 𝔠
source
@[simp]
theorem cardinal.continuum_add_self  :
𝔠 + 𝔠 = 𝔠
source
@[simp]
theorem cardinal.nat_add_continuum (n : ℕ) :
↑n + 𝔠 = 𝔠
source
@[simp]
theorem cardinal.continuum_add_nat (n : ℕ) :
𝔠 + ↑n = 𝔠

Multiplication #

source
@[simp]
theorem cardinal.continuum_mul_self  :
𝔠 * 𝔠 = 𝔠
source
@[simp]
theorem cardinal.continuum_mul_omega  :
𝔠 * ω = 𝔠
source
@[simp]
theorem cardinal.omega_mul_continuum  :
ω * 𝔠 = 𝔠
source
@[simp]
theorem cardinal.nat_mul_continuum {n : ℕ} (hn : n ≠ 0) :
(↑n) * 𝔠 = 𝔠
source
@[simp]
theorem cardinal.continuum_mul_nat {n : ℕ} (hn : n ≠ 0) :
𝔠 * ↑n = 𝔠

Power #

source
@[simp]
theorem cardinal.omega_power_omega  :
ω ^ ω = 𝔠
source
@[simp]
theorem cardinal.nat_power_omega {n : ℕ} (hn : 2 ≤ n) :
↑n ^ ω = 𝔠
source
@[simp]
theorem cardinal.continuum_power_omega  :
𝔠 ^ ω = 𝔠