mathlib3 documentation

set_theory.cardinal.continuum

Cardinality of continuum #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_aleph_0  :
2 ^ cardinal.aleph_0 = cardinal.continuum
source
@[simp]
theorem cardinal.lift_continuum  :
cardinal.continuum.lift = cardinal.continuum

Inequalities #

source
@[simp]
theorem cardinal.continuum_le_lift {c : cardinal} :
cardinal.continuum ≀ c.lift ↔ cardinal.continuum ≀ c
source
@[simp]
theorem cardinal.lift_le_continuum {c : cardinal} :
c.lift ≀ cardinal.continuum ↔ c ≀ cardinal.continuum
source
@[simp]
theorem cardinal.continuum_lt_lift {c : cardinal} :
cardinal.continuum < c.lift ↔ cardinal.continuum < c
source
@[simp]
theorem cardinal.lift_lt_continuum {c : cardinal} :
c.lift < cardinal.continuum ↔ c < cardinal.continuum
source
theorem cardinal.aleph_0_lt_continuum  :
cardinal.aleph_0 < cardinal.continuum
source
theorem cardinal.aleph_0_le_continuum  :
cardinal.aleph_0 ≀ 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_to_nat  :
⇑cardinal.to_nat cardinal.continuum = 0
source
@[simp]
theorem cardinal.continuum_to_part_enat  :
⇑cardinal.to_part_enat cardinal.continuum = ⊀

Addition #

source
@[simp]
theorem cardinal.aleph_0_add_continuum  :
cardinal.aleph_0 + cardinal.continuum = cardinal.continuum
source
@[simp]
theorem cardinal.continuum_add_aleph_0  :
cardinal.continuum + cardinal.aleph_0 = 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_aleph_0  :
cardinal.continuum * cardinal.aleph_0 = cardinal.continuum
source
@[simp]
theorem cardinal.aleph_0_mul_continuum  :
cardinal.aleph_0 * 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.aleph_0_power_aleph_0  :
cardinal.aleph_0 ^ cardinal.aleph_0 = cardinal.continuum
source
@[simp]
theorem cardinal.nat_power_aleph_0 {n : β„•} (hn : 2 ≀ n) :
↑n ^ cardinal.aleph_0 = cardinal.continuum
source
@[simp]
theorem cardinal.continuum_power_aleph_0  :
cardinal.continuum ^ cardinal.aleph_0 = cardinal.continuum