mathlib documentation

set_theory.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 #

Cardinality of continuum.

Equations

Inequalities #

Addition #

Multiplication #

Power #