aleph_max

Mathlib.SetTheory.Cardinal.Aleph

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

English

For all ordinals o1, o2, we have ℵ_(max(o1,o2)) = max(ℵ_(o1), ℵ_(o2)).

Русский

Для любых ординалов o1, o2 выполняется ℵ_(max(o1,o2)) = max(ℵ_(o1), ℵ_(o2)).

LaTeX

$$$$ \aleph_{\max(o_1,o_2)} = \max(\aleph_{o_1}, \aleph_{o_2}). $$$$

Lean4

theorem aleph_max (o₁ o₂ : Ordinal) : ℵ_ (max o₁ o₂) = max (ℵ_ o₁) (ℵ_ o₂) :=
  aleph.monotone.map_max

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

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

Разделы

Аффилиация

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