aleph0_toNat

Mathlib.SetTheory.Cardinal.ToNat

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

English

The cardinality of the natural numbers, aleph_0, maps to 0 under toNat: toNat(aleph0) = 0.

Русский

Кардинал ℵ0 соответствует 0 под toNat: toNat(ℵ0) = 0.

LaTeX

$$$\operatorname{toNat}(\aleph_0) = 0.$$$

Lean4

@[simp]
theorem aleph0_toNat : toNat ℵ₀ = 0 :=
  toNat_apply_of_aleph0_le le_rfl

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

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

Разделы

Аффилиация

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