aleph0_mul_aleph

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

ℵ0 × ℵ_o = ℵ_o for any ordinal o.

Русский

ℵ₀ × ℵ_o = ℵ_o для любого ординала o.

LaTeX

$$$\aleph_0 \cdot \aleph_{o} = \aleph_{o}$$$

Lean4

@[simp]
theorem aleph0_mul_aleph (o : Ordinal) : ℵ₀ * ℵ_ o = ℵ_ o :=
  aleph0_mul_eq (aleph0_le_aleph o)

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

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

Разделы

Аффилиация

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