aleph_add_aleph

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

For ordinals o1,o2, ℵ_{o1} + ℵ_{o2} = ℵ_{max(o1,o2)}.

Русский

Для ординалов o1, o2 верно ℵ_{o1} + ℵ_{o2} = ℵ_{max(o1,o2)}.

LaTeX

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

Lean4

@[simp]
theorem aleph_add_aleph (o₁ o₂ : Ordinal) : ℵ_ o₁ + ℵ_ o₂ = ℵ_ (max o₁ o₂) := by
  rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), aleph_max]

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

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

Разделы

Аффилиация

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