isStrongLimit_beth

Mathlib.SetTheory.Cardinal.Aleph

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

← MathLib Explorer

English

For all o, IsStrongLimit(beth(o)) iff IsSuccPrelimit(o).

Русский

Для любого o верно IsStrongLimit(beth(o)) ⇔ IsSuccPrelimit(o).

LaTeX

$$$\operatorname{IsStrongLimit}(\beth(o)) \iff \operatorname{IsSuccPrelimit}(o)$$$

Lean4

theorem isStrongLimit_beth {o : Ordinal} : IsStrongLimit (ℶ_ o) ↔ IsSuccPrelimit o := by
  rw [beth_eq_preBeth, isStrongLimit_preBeth, isSuccLimit_add_iff_of_isSuccLimit isSuccLimit_omega0]

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

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

Разделы

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

Аффилиация

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