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 #

Cardinality of continuum.

Equations
@[simp]

Inequalities #

Addition #

@[simp]
@[simp]

Multiplication #

@[simp]
theorem cardinal.nat_mul_continuum {n : } (hn : n 0) :
@[simp]
theorem cardinal.continuum_mul_nat {n : } (hn : n 0) :

Power #

@[simp]
@[simp]
theorem cardinal.nat_power_omega {n : } (hn : 2 n) :