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 #

𝔠 : notation for Cardinal.continuum in locale Cardinal.

source

def Cardinal.continuum :

Cardinal.{u}

Cardinality of continuum.

Equations

Cardinal.continuum = 2 ^ Cardinal.aleph0

Instances For

source

def Cardinal.term𝔠 :

Lean.ParserDescr

Equations

Cardinal.term𝔠 = Lean.ParserDescr.node `Cardinal.term𝔠 1024 (Lean.ParserDescr.symbol "𝔠")

Instances For

source

@[simp]

theorem Cardinal.two_power_aleph0 :

2 ^ Cardinal.aleph0 = Cardinal.continuum

source

@[simp]

theorem Cardinal.lift_continuum :

Cardinal.lift.{v, u_1} Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_le_lift {c : Cardinal.{u}} :

Cardinal.continuum ≤ Cardinal.lift.{v, u} c ↔ Cardinal.continuum ≤ c

source

@[simp]

theorem Cardinal.lift_le_continuum {c : Cardinal.{u}} :

Cardinal.lift.{v, u} c ≤ Cardinal.continuum ↔ c ≤ Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_lt_lift {c : Cardinal.{u}} :

Cardinal.continuum < Cardinal.lift.{v, u} c ↔ Cardinal.continuum < c

source

@[simp]

theorem Cardinal.lift_lt_continuum {c : Cardinal.{u}} :

Cardinal.lift.{v, u} c < Cardinal.continuum ↔ c < Cardinal.continuum

Inequalities #

source

theorem Cardinal.aleph0_lt_continuum :

Cardinal.aleph0 < Cardinal.continuum

source

theorem Cardinal.aleph0_le_continuum :

Cardinal.aleph0 ≤ Cardinal.continuum

source

@[simp]

theorem Cardinal.beth_one :

Cardinal.beth 1 = Cardinal.continuum

source

theorem Cardinal.nat_lt_continuum (n : ℕ) :

↑n < Cardinal.continuum

source

theorem Cardinal.mk_set_nat :

Cardinal.mk (Set ℕ) = Cardinal.continuum

source

theorem Cardinal.continuum_pos :

0 < Cardinal.continuum

source

theorem Cardinal.continuum_ne_zero :

Cardinal.continuum ≠ 0

source

theorem Cardinal.aleph_one_le_continuum :

Cardinal.aleph 1 ≤ Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_toNat :

↑Cardinal.toNat Cardinal.continuum = 0

source

@[simp]

theorem Cardinal.continuum_toPartENat :

↑Cardinal.toPartENat Cardinal.continuum = ⊤

Addition #

source

@[simp]

theorem Cardinal.aleph0_add_continuum :

Cardinal.aleph0 + Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_add_aleph0 :

Cardinal.continuum + Cardinal.aleph0 = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_add_self :

Cardinal.continuum + Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.nat_add_continuum (n : ℕ) :

↑n + Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_add_nat (n : ℕ) :

Cardinal.continuum + ↑n = Cardinal.continuum

Multiplication #

source

@[simp]

theorem Cardinal.continuum_mul_self :

Cardinal.continuum * Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_mul_aleph0 :

Cardinal.continuum * Cardinal.aleph0 = Cardinal.continuum

source

@[simp]

theorem Cardinal.aleph0_mul_continuum :

Cardinal.aleph0 * Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.nat_mul_continuum {n : ℕ} (hn : n ≠ 0) :

↑n * Cardinal.continuum = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_mul_nat {n : ℕ} (hn : n ≠ 0) :

Cardinal.continuum * ↑n = Cardinal.continuum

Power #

source

@[simp]

theorem Cardinal.aleph0_power_aleph0 :

Cardinal.aleph0 ^ Cardinal.aleph0 = Cardinal.continuum

source

@[simp]

theorem Cardinal.nat_power_aleph0 {n : ℕ} (hn : 2 ≤ n) :

↑n ^ Cardinal.aleph0 = Cardinal.continuum

source

@[simp]

theorem Cardinal.continuum_power_aleph0 :

Cardinal.continuum ^ Cardinal.aleph0 = Cardinal.continuum