mathlib documentation


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 #

Cardinality of continuum.


Inequalities #

Addition #

Multiplication #

Power #