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 the continuum.

Equations
Instances For
    Equations
    Instances For

      Inequalities #

      @[simp]

      Addition #

      Multiplication #

      Power #