The cardinality of the complex numbers

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

@[simp]

theorem Cardinal.mk_complex : mk ℂ = continuum

The cardinality of the complex numbers, as a type.

@[deprecated Cardinal.mk_complex (since := "2025-03-13")]

theorem mk_complex : Cardinal.mk ℂ = Cardinal.continuum

Alias of Cardinal.mk_complex.

---

The cardinality of the complex numbers, as a type.

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

The cardinality of the complex numbers, as a set.

@[deprecated Cardinal.mk_univ_complex (since := "2025-03-13")]

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

Alias of Cardinal.mk_univ_complex.

---

The cardinality of the complex numbers, as a set.

theorem not_countable_complex : ¬Set.univ.Countable

The complex numbers are not countable.