not_countable_real

Mathlib.Analysis.Real.Cardinality

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

English

The real numbers are not countable.

Русский

Действительные числа не счетны.

LaTeX

$$$\neg (\mathrm{Set.univ} : \mathrm{Set}\,\mathbb{R}).Countable$$$

Lean4

theorem not_countable_real : ¬(Set.univ : Set ℝ).Countable :=
  not_countable_univ

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

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

Разделы

Аффилиация

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