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 forCardinal.continuum
in localeCardinal
.
@[simp]
@[simp]
@[simp]
@[simp]
Inequalities #
@[simp]
Addition #
@[simp]
@[simp]
@[simp]
@[simp]
Multiplication #
@[simp]
@[simp]
@[simp]
@[simp]
Power #
@[simp]
@[simp]