isRegular_cof

Mathlib.SetTheory.Cardinal.Regular

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

English

If o is a succ-limit, then o.cof is regular.

Русский

Если o — предельно-наследованный предел, то o.cof — регулярный.

LaTeX

$$$IsRegular(o.cof).$$$

Lean4

theorem isRegular_cof {o : Ordinal} (h : IsSuccLimit o) : IsRegular o.cof :=
  ⟨aleph0_le_cof.2 h, (cof_cof o).ge⟩

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

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

Разделы

Аффилиация

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