omega_max

Mathlib.SetTheory.Cardinal.Aleph

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

English

For all ordinals o1 and o2, the omega indexed at the maximum equals the maximum of the omegas: ω_{max(o1,o2)} = max(ω_{o1}, ω_{o2}).

Русский

Для любых ординалов o1, o2 верно: ω_{max(o1,o2)} = max(ω_{o1}, ω_{o2}).

LaTeX

$$$ \omega_{\max(o_1,o_2)} = \max(\omega_{o_1}, \omega_{o_2}) $$$

Lean4

theorem omega_max (o₁ o₂ : Ordinal) : ω_ (max o₁ o₂) = max (ω_ o₁) (ω_ o₂) :=
  omega.monotone.map_max

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

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

Разделы

Аффилиация

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