isRegular_aleph_succ

Mathlib.SetTheory.Cardinal.Regular

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

English

IsRegular aleph_succ (succ o).

Русский

IsRegular aleph_succ (succ o).

LaTeX

$$IsRegular(aleph_succ(succ\, o)).$$

Lean4

theorem isRegular_aleph_succ (o : Ordinal) : IsRegular (ℵ_ (succ o)) :=
  by
  rw [aleph_succ]
  exact isRegular_succ (aleph0_le_aleph o)

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

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

Разделы

Аффилиация

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