not_countable_complex

Mathlib.Analysis.Complex.Cardinality

URI: https://scilib.ai/kg/mathlib#not_countable_complex

← MathLib Explorer

English

The set of all complex numbers is not countable.

Русский

Множество всех комплексных чисел несчётно.

LaTeX

$$|\u2113| \\neq aleph_0$$

Lean4

/-- The complex numbers are not countable. -/
theorem not_countable_complex : ¬(Set.univ : Set ℂ).Countable :=
  by
  rw [← le_aleph0_iff_set_countable, not_le, Cardinal.mk_univ_complex]
  apply cantor

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru