aleph0_mul_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

ℵ₀ * m = ℵ₀ for nonzero ENat m.

Русский

ℵ₀ · m = ℵ₀ при m ≠ 0.

LaTeX

$$$\\aleph_0 \\cdot m = \\aleph_0 \\quad \\text{при } m \\neq 0$$$

Lean4

@[simp]
theorem aleph0_mul_ofENat {m : ℕ∞} (hm : m ≠ 0) : ℵ₀ * m = ℵ₀ := by rw [mul_comm, ofENat_mul_aleph0 hm]

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

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

Разделы

Аффилиация

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