aleph0_add_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

ℵ₀ + m = ℵ₀ for any ENat m.

Русский

ℵ₀ + m = ℵ₀ для любого m ∈ ℕ∞.

LaTeX

$$$\\aleph_0 + m = \\aleph_0$$$

Lean4

@[simp]
theorem aleph0_add_ofENat (m : ℕ∞) : ℵ₀ + m = ℵ₀ :=
  (ofENat_add ⊤ m).symm

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

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

Разделы

Аффилиация

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