mk_univ_complex

Mathlib.Analysis.Complex.Cardinality

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_univ_complex

English

The complex numbers have the same cardinality as the real continuum; |ℂ| = c.

Русский

Множество комплексных чисел эквивалентно континууму; |ℂ| = c.

LaTeX

$$|\u2116|\\mathbb{C}| = \\mathfrak{c}$$

Lean4

/-- The cardinality of the complex numbers, as a set. -/
theorem mk_univ_complex : #(Set.univ : Set ℂ) = 𝔠 := by rw [mk_univ, mk_complex]

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

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

Разделы

Аффилиация

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