Documentation

Mathlib.SetTheory.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
Instances For
    Equations
    Instances For

      Inequalities #

      Addition #

      Multiplication #

      Power #