isSuccPrelimit

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.IsStrongLimit.isSuccPrelimit

English

If c is a strong limit cardinal, then c is a succ-prelimit.

Русский

Если c — сильный предел кардинал, то он является succ-предпределительным.

LaTeX

$$$\\forall c\\ (H : IsStrongLimit c)\\, IsSuccPrelimit\\, c$$$

Lean4

protected theorem isSuccPrelimit {c} (H : IsStrongLimit c) : IsSuccPrelimit c :=
  H.isSuccLimit.isSuccPrelimit

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

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

Разделы

Аффилиация

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