isInitial_preOmega

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Ordinal.isInitial_preOmega

English

For every ordinal o, preOmega(o) is initial.

Русский

Для любого ординала o preOmega(o) является начальным.

LaTeX

$$$\mathrm{IsInitial}(\mathrm{preOmega}(o))$$$

Lean4

theorem isInitial_preOmega (o : Ordinal) : IsInitial (preOmega o) :=
  enumOrd_mem not_bddAbove_isInitial o

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

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

Разделы

Аффилиация

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