aleph0_lt_aleph_one

Mathlib.SetTheory.Cardinal.Aleph

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

English

The first infinite cardinal is strictly less than the next one: ℵ₀ < ℵ₁.

Русский

Первая бесконечная кардинальность строго меньше следующей: ℵ₀ < ℵ₁.

LaTeX

$$$\aleph_0 < \aleph_1$$$

Lean4

theorem aleph0_lt_aleph_one : ℵ₀ < ℵ₁ := by
  rw [← succ_aleph0]
  apply lt_succ

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

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

Разделы

Аффилиация

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