isSuccLimit_aleph0

Mathlib.SetTheory.Cardinal.Basic

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

English

aleph0 is a successor-limit cardinal.

Русский

aleph0 — предельный предел следующего (IsSuccLimit).

LaTeX

$$$\text{IsSuccLimit}(\aleph_0)$$$

Lean4

theorem isSuccLimit_aleph0 : IsSuccLimit ℵ₀ :=
  by
  rw [Cardinal.isSuccLimit_iff]
  exact ⟨aleph0_ne_zero, isSuccPrelimit_aleph0⟩

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

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

Разделы

Аффилиация

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