mk_nat

Mathlib.SetTheory.Cardinal.Defs

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

English

The cardinality of the natural numbers equals aleph-null: |ℕ| = aleph_0.

Русский

Кардинал множества чисел натурального множества равен алеф-ноль: |ℕ| = aleph_0.

LaTeX

$$$ |\mathbb{N}| = \aleph_{0} $$$

Lean4

theorem mk_nat : #ℕ = ℵ₀ :=
  (lift_id _).symm

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

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

Разделы

Аффилиация

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