Documentation

Mathlib.Data.Complex.Cardinality

The cardinality of the complex numbers #

This file shows that the complex numbers have cardinality continuum, i.e. #ℂ = 𝔠.

source
@[simp]
theorem mk_complex :
Cardinal.mk ℂ = Cardinal.continuum

The cardinality of the complex numbers, as a type.

source
theorem mk_univ_complex :
Cardinal.mk ↑Set.univ = Cardinal.continuum

The cardinality of the complex numbers, as a set.

source
theorem not_countable_complex :
¬Set.Countable Set.univ

The complex numbers are not countable.