mathlib3 documentation

data.complex.cardinality

The cardinality of the complex numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[simp]
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.univ.countable

The complex numbers are not countable.