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
.
Cardinality of continuum.
Equations
Instances For
Equations
- Cardinal.termπ = Lean.ParserDescr.node `Cardinal.termπ 1024 (Lean.ParserDescr.symbol "π ")
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
Inequalities #
@[simp]
Addition #
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Multiplication #
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Power #
@[simp]
@[simp]