ord_aleph

Mathlib.SetTheory.Cardinal.Aleph

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

English

The ordinal of the cardinal ℵ_o is ω_o.

Русский

Порядок (ординал) кардинала ℵ_o равен ω_o.

LaTeX

$$$$ \operatorname{ord}(\aleph_{o}) = \omega_{o}. $$$$

Lean4

@[simp]
theorem ord_aleph (o : Ordinal) : (ℵ_ o).ord = ω_ o :=
  ord_preAleph _

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

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

Разделы

Аффилиация

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