ord_preAleph

Mathlib.SetTheory.Cardinal.Aleph

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

English

The order type of preAleph(o) equals preOmega(o).

Русский

Порядковый тип preAleph(o) равен preOmega(o).

LaTeX

$$$ \operatorname{ord}(\text{preAleph}(o)) = \text{preOmega}(o) $$$

Lean4

@[simp]
theorem ord_preAleph (o : Ordinal) : (preAleph o).ord = preOmega o := by
  rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]

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

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

Разделы

Аффилиация

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