Documentation

Mathlib.SetTheory.Cardinal.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.{u}

Cardinality of continuum.

Equations
source
def Cardinal.term𝔠 :
Lean.ParserDescr
Equations
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
source
@[simp]
theorem Cardinal.ofNat_add_continuum {n : β„•} [n.AtLeastTwo] :
OfNat.ofNat n + Cardinal.continuum = Cardinal.continuum
source
@[simp]
theorem Cardinal.continuum_add_ofNat {n : β„•} [n.AtLeastTwo] :
Cardinal.continuum + OfNat.ofNat 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
source
@[simp]
theorem Cardinal.ofNat_mul_continuum {n : β„•} [n.AtLeastTwo] :
OfNat.ofNat n * Cardinal.continuum = Cardinal.continuum
source
@[simp]
theorem Cardinal.continuum_mul_ofNat {n : β„•} [n.AtLeastTwo] :
Cardinal.continuum * OfNat.ofNat 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
source
theorem Cardinal.power_aleph0_of_le_continuum {x : Cardinal.{u_1}} (h₁ : 2 ≀ x) (hβ‚‚ : x ≀ Cardinal.continuum) :
x ^ Cardinal.aleph0 = Cardinal.continuum