isRegular_preAleph_succ

Mathlib.SetTheory.Cardinal.Regular

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

← MathLib Explorer

English

If ω ≤ o, then preAleph(succ o) is regular.

Русский

Если ω ≤ o, то preAleph(succ o) регулярный.

LaTeX

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

Lean4

theorem isRegular_preAleph_succ {o : Ordinal} (h : ω ≤ o) : IsRegular (preAleph (succ o)) :=
  by
  rw [preAleph_succ]
  exact isRegular_succ (aleph0_le_preAleph.2 h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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