isNormal_omega

Mathlib.SetTheory.Cardinal.Aleph

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

English

ω is a normal ordinal.

Русский

ω является нормальным ординалом.

LaTeX

$$$ \text{IsNormal}(\omega) $$$

Lean4

theorem isNormal_omega : IsNormal omega :=
  isNormal_preOmega.trans (isNormal_add_right _)

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

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

Разделы

Аффилиация

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