aleph_zero

Mathlib.SetTheory.Cardinal.Aleph

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

English

The index-0 aleph equals the first infinite cardinal: ℵ_0 = ℵ₀.

Русский

Индекс ноль в aleph совпадает с первым бесконечным кардиналом: ℵ_0 = ℵ₀.

LaTeX

$$$$ \aleph_{0} = \aleph_{0}. $$$$

Lean4

@[simp]
theorem aleph_zero : ℵ_ 0 = ℵ₀ := by rw [aleph_eq_preAleph, add_zero, preAleph_omega0]

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

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

Разделы

Аффилиация

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