mk_mul_aleph0_eq

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

For infinite α, #α × ℵ0 = #α.

Русский

Для бесконечного α верно: |α| × ℵ0 = |α|.

LaTeX

$$#α \cdot \aleph_0 = #\alpha$$

Lean4

theorem mk_mul_aleph0_eq {α : Type*} [Infinite α] : #α * ℵ₀ = #α :=
  mul_aleph0_eq (aleph0_le_mk α)

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

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

Разделы

Аффилиация

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